English
For a separable finite extension K ⊂ L with a power basis, the determinant of the trace matrix is nonzero.
Русский
Для развоплощенного конечного расширения K ⊂ L с базисом мощности детерминант матрицы следа не равен нулю.
LaTeX
$$$\\det(\\mathrm{traceMatrix}(K,\\text{pb.basis})) \\neq 0$$$
Lean4
theorem det_traceMatrix_ne_zero' [Algebra.IsSeparable K L] : det (traceMatrix K pb.basis) ≠ 0 :=
by
suffices algebraMap K (AlgebraicClosure L) (det (traceMatrix K pb.basis)) ≠ 0
by
refine mt (fun ht => ?_) this
rw [ht, RingHom.map_zero]
haveI : FiniteDimensional K L := pb.finite
let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm
· rw [RingHom.map_det, RingHom.mapMatrix_apply, traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]
refine mt mul_self_eq_zero.mp ?_
simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]
rintro i ⟨_, j, hij, h⟩
exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)
· rw [AlgHom.card, pb.finrank]
