trace_ne_zero — Mathlib

English

Let pb be a power basis K,L with K,L finite and separable; then det(traceMatrix(K,pb.basis)) ≠ 0.

Русский

Пусть pb — базис мощности K ⊂ L, где K ⊂ L конечно и разделяемо; тогда det(traceMatrix(K, pb.basis)) ≠ 0.

LaTeX

$$$\\det(\\mathrm{traceMatrix}(K,\\text{pb.basis})) \\neq 0$$$

Lean4

theorem trace_ne_zero [FiniteDimensional K L] [Algebra.IsSeparable K L] : Algebra.trace K L ≠ 0 :=
  ((traceForm_nondegenerate_tfae K L).out 0 1).mp ‹_›

Похожие утверждения