discr_not_zero_of_basis — Mathlib

English

If b is a basis of a finite separable extension L/K, then discr K b ≠ 0.

Русский

Если b является базисом конечного раздельного расширения L/K, то дискриминант не равен нулю.

LaTeX

$$discr K b ≠ 0$$

Lean4

/-- If `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b ≠ 0`. -/
theorem discr_not_zero_of_basis [Algebra.IsSeparable K L] (b : Basis ι K L) : discr K b ≠ 0 :=
  by
  rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero]
  exact traceForm_nondegenerate _ _

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