Theorems · Theorem · commutative algebra

Algebra.discr_eq_discr_of_algEquiv

∀ {A : Type u} {B : Type v} {C : Type z} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : CommRing C] [inst_5 : Algebra A C] [inst_6 : Fintype ι] (b : ι → B) (f : B ≃ₐ[A] C),
  Algebra.discr A b = Algebra.discr A (⇑f ∘ b)

Mapping a family of vectors along an AlgEquiv preserves the discriminant.

Defined in

Mathlib.RingTheory.Discriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqCommRingCommRingAlgebraCommRingAlgebraFintype