Theorems · Definition · commutative algebra

Algebra.discr

{ι : Type w} →
  [DecidableEq ι] →
    (A : Type u) →
      {B : Type v} → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → [Fintype ι] → (ι → B) → A

Given an A-algebra B and b, an ι-indexed family of elements of B, we define discr A ι b as the determinant of traceMatrix A ι b.

Defined in

Mathlib.RingTheory.Discriminant

Cited by

38 results in Mathlib

Foundations

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

Assumes

DecidableEqCommRingCommRingAlgebraFintype