Theorems · Theorem · commutative algebra

Algebra.discr_eq_discr

∀ (A : Type u) {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : Fintype ι]
  (b b' : Module.Basis ι ℤ A), Algebra.discr ℤ ⇑b = Algebra.discr ℤ ⇑b'

Two (finite) ℤ-bases have the same discriminant.

Defined in

Mathlib.RingTheory.Discriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqCommRingFintype