English
If L/K is finite and separable, then the trace form is nondegenerate; equivalently, some matrices associated to traces are invertible.
Русский
Если расширение L/K конечное и разделяемое, форма следа не вырождена; эквивалентно тому, что некоторые матрицы следа обратимы.
LaTeX
$$$\\operatorname{traceForm}(K,L) \\text{ is nondegenerate} \\iff \\det(\\mathrm{traceMatrix}(K,\\text{pb.basis})) \\neq 0$$$
Lean4
/-- Let $L/K$ be a finite extension of fields. If $L/K$ is separable,
then `traceForm` is nondegenerate. -/
@[stacks 0BIL "(1) => (3)"]
theorem traceForm_nondegenerate [FiniteDimensional K L] [Algebra.IsSeparable K L] : (traceForm K L).Nondegenerate :=
BilinForm.nondegenerate_of_det_ne_zero (traceForm K L) _ (det_traceForm_ne_zero (Module.finBasis K L))
