From 1f7c3c78e42e453ecd9a8992f25cf081d18f5406 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 10 Jul 2026 23:35:13 +0100 Subject: [PATCH 1/2] Add --- Mathlib/NumberTheory/Height/NumberField.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean index 852c8132ed30e9..edafa054e79a48 100644 --- a/Mathlib/NumberTheory/Height/NumberField.lean +++ b/Mathlib/NumberTheory/Height/NumberField.lean @@ -128,6 +128,15 @@ lemma mulHeight_eq {ι : Type*} {x : ι → K} (hx : x ≠ 0) : simp only [FinitePlace.coe_apply, InfinitePlace.coe_apply, Height.mulHeight_eq hx, prod_archAbsVal_eq, prod_nonarchAbsVal_eq fun v ↦ ⨆ i, v (x i)] +open Classical IntermediateField in +/-- The absolute multiplicative height of an algebraic number. -/ +noncomputable def absMulHeight₁ {K : Type*} [Field K] [CharZero K] (x : K) : ℝ := + if hx : IsIntegral ℚ x then + haveI : FiniteDimensional ℚ ℚ⟮x⟯ := adjoin.finiteDimensional hx + haveI : NumberField ℚ⟮x⟯ := {} + (Height.mulHeight₁ (AdjoinSimple.gen ℚ x)) ^ (Module.finrank ℚ ℚ⟮x⟯ : ℝ)⁻¹ + else 0 + variable (K) in lemma totalWeight_eq_sum_mult : totalWeight K = ∑ v : InfinitePlace K, v.mult := by simp only [totalWeight] From f75c115ba1d5e95a1267958567aa9f48629b80cb Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 10 Jul 2026 23:40:39 +0100 Subject: [PATCH 2/2] better docstring --- Mathlib/NumberTheory/Height/NumberField.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean index edafa054e79a48..662998281a7a86 100644 --- a/Mathlib/NumberTheory/Height/NumberField.lean +++ b/Mathlib/NumberTheory/Height/NumberField.lean @@ -129,7 +129,8 @@ lemma mulHeight_eq {ι : Type*} {x : ι → K} (hx : x ≠ 0) : prod_archAbsVal_eq, prod_nonarchAbsVal_eq fun v ↦ ⨆ i, v (x i)] open Classical IntermediateField in -/-- The absolute multiplicative height of an algebraic number. -/ +/-- The absolute multiplicative height of an algebraic number. This is defined for elements of any +field of characteristic zero, with a junk value of `0` if the element is not algebraic. -/ noncomputable def absMulHeight₁ {K : Type*} [Field K] [CharZero K] (x : K) : ℝ := if hx : IsIntegral ℚ x then haveI : FiniteDimensional ℚ ℚ⟮x⟯ := adjoin.finiteDimensional hx