English
The determinant of the basis matrix is nonzero; equivalently, the basis matrix is invertible.
Русский
Определитель базисной матрицы ненулевой; следовательно, матрица базиса обратима.
LaTeX
$$$$\\det(\\text{basisMatrix}(K)) \\neq 0.$$$$
Lean4
theorem det_of_basisMatrix_non_zero [DecidableEq (K →+* ℂ)] : (basisMatrix K).det ≠ 0 :=
by
let e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom
rw [show (basisMatrix K) = N by ext : 2; simp only [N, latticeBasis_apply, integralBasis_apply, of_apply, apply_at];
rfl,
← pow_ne_zero_iff two_ne_zero]
convert (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
exact
(Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ (fun _ => integralBasis K (e _))
RingHom.equivRatAlgHom).symm
