Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Co-authored-by: Michael Stoll <[email protected]>
leanprover-community · Dec 3, 2024 · 5b8d18a · 5b8d18a
1 parent bea3cb8
commit 5b8d18a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean
@@ -151,7 +151,7 @@ instance : MonoidWithZeroHomClass (FinitePlace K) K ℝ where
   map_zero w := w.1.map_zero
 
 instance : NonnegHomClass (FinitePlace K) K ℝ where
-  apply_nonneg w _ := w.1.nonneg _
+  apply_nonneg w := w.1.nonneg
 
 @[simp]
 theorem apply (v : HeightOneSpectrum (𝓞 K)) (x : K) : mk v x =  ‖embedding v x‖ := rfl