Theorems · Theorem · commutative algebra

Algebra.discr_isUnit_of_basis

∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] (b : Module.Basis ι K L),
  IsUnit (Algebra.discr K ⇑b)

If b is a basis of a finite separable field extension L/K, then Algebra.discr K b is a unit.

Defined in

Mathlib.RingTheory.Discriminant

Cited by

2 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeFieldFieldAlgebraModule.FiniteAlgebra.IsSeparable