discr_isUnit_of_basis — Mathlib

English

If b is a basis of a finite separable extension, then discr K b is a unit in the base ring.

Русский

Если b — базис конечного раздельного расширения, дискриминант является единицей в базовом кольце.

LaTeX

$$IsUnit (discr K b)$$

Lean4

/-- If `b` is a basis of a finite separable field extension `L/K`,
  then `Algebra.discr K b` is a unit. -/
theorem discr_isUnit_of_basis [Algebra.IsSeparable K L] (b : Basis ι K L) : IsUnit (discr K b) :=
  IsUnit.mk0 _ (discr_not_zero_of_basis _ _)

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