Theorems · Theorem · commutative algebra

Algebra.discr_powerBasis_eq_norm

∀ (K : Type u) {L : Type v} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Module.Finite K L]
  (pb : PowerBasis K L) [Algebra.IsSeparable K L],
  Algebra.discr K ⇑pb.basis =
    (-1) ^ (Module.finrank K L * (Module.finrank K L - 1) / 2) *
      (Algebra.norm K) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen)))

Formula for the discriminant of a power basis using the norm of the field extension.

Defined in

Mathlib.RingTheory.Discriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraModule.FiniteAlgebra.IsSeparable