English
Discriminant is independent of the choice of an integer ℤ-basis of a finite free ℤ-module. If b,b' are two ℤ-bases of a finite free ℤ-module A, then discr ℤ b = discr ℤ b'.
Русский
Дискриминант не зависит от выбора базиса ℤ-базиса конечного свободного модуля над ℤ: если b и b' — два ℤ-базиса A, тогда дискриминант discr ℤ b равен discr ℤ b'.
LaTeX
$$$$ \\mathrm{discr}\\,\\mathbb{Z}\\;b = \\mathrm{discr}\\,\\mathbb{Z}\\;b' $$$$
Lean4
/-- Two (finite) ℤ-bases have the same discriminant. -/
theorem discr_eq_discr (b : Basis ι ℤ A) (b' : Basis ι ℤ A) : Algebra.discr ℤ b = Algebra.discr ℤ b' :=
by
convert Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)
· rw [Basis.toMatrix_map_vecMul]
· suffices IsUnit (b'.toMatrix b).det
by
rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
rw [this, one_mul]
rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']
exact LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'
