English
If f is an algebra equivalence, then discr K equals discr L; same principle as 152021 but under a different formulation.
Русский
Если f — алгебраическая эквиволентность, то discr K = discr L; аналогично 152021.
LaTeX
$$$$\\operatorname{discr} K = \\operatorname{discr} L$$$$
Lean4
/-- The absolute discriminant of the number field `ℚ` is 1. -/
@[simp]
theorem numberField_discr : discr ℚ = 1 :=
by
let b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
Basis.map (Basis.singleton (Fin 1) ℤ) ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
calc
NumberField.discr ℚ
_ = Algebra.discr ℤ b := by convert (discr_eq_discr ℚ b).symm
_ = Algebra.trace ℤ (𝓞 ℚ) (b default * b default) := by
rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
_ = Algebra.trace ℤ (𝓞 ℚ) 1 := by
rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, ← AddEquiv.toIntLinearEquiv_symm, AddEquiv.coe_toIntLinearEquiv,
Basis.singleton_apply, show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
map_one, mul_one]
_ = 1 := by rw [Algebra.trace_eq_matrix_trace b]; simp
