Theorems · Theorem · commutative algebra

Algebra.discr_isIntegral

∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Algebra K L] [Module.Finite K L] {R : Type z} [inst_6 : CommRing R]
  [inst_7 : Algebra R K] [inst_8 : Algebra R L] [IsScalarTower R K L] {b : ι → L},
  (∀ (i : ι), IsIntegral R (b i)) → IsIntegral R (Algebra.discr K b)

If K and L are fields and IsScalarTower R K L, and b : ι → L satisfies ∀ i, IsIntegral R (b i), then IsIntegral R (discr K b).

Defined in

Mathlib.RingTheory.Discriminant

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeFieldFieldAlgebraModule.FiniteCommRingAlgebraAlgebraIsScalarTower