Theorems · Theorem · commutative algebra

Algebra.discr_powerBasis_eq_prod

∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E] [inst_3 : Algebra K L]
  [inst_4 : Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) (e : Fin pb.dim ≃ (L →ₐ[K] E))
  [Algebra.IsSeparable K L],
  (algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

The discriminant of a power basis.

Defined in

Mathlib.RingTheory.Discriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraModule.FiniteIsAlgClosedAlgebra.IsSeparable