From 5b8d18a80eb48f5d1a37ee79a92872fe98896860 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:29:26 +0100 Subject: [PATCH] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index ed4a302e2820c..00607d5ddd2af 100644 --- 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