English
A supplementary form of the previous determinant relation linking a refined basis to absNorm.
Русский
Дополнительная форма соотношения детерминант между более точными базисами и absNorm.
LaTeX
$$An auxiliary identity accompanying AbsDetBasisChange for refined bases.$$
Lean4
@[simp]
theorem absNorm_span_singleton [Module.Finite ℚ K] (x : K) : absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ x)| :=
by
have : IsDomain K := IsFractionRing.isDomain R
obtain ⟨d, ⟨r, hr⟩⟩ := IsLocalization.exists_integer_multiple R⁰ x
rw [absNorm_eq' d (Ideal.span { r })]
· rw [Ideal.absNorm_span_singleton]
simp_rw [Int.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ (Algebra.norm ℤ _) by rfl, ←
Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]
rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc,
mul_div_cancel₀ _
(by
rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
exact nonZeroDivisors.coe_ne_zero _)]
· ext
simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and, map_mul, hr, ←
Algebra.smul_def, smul_comm (d : R)]
