Theorems · Theorem · commutative algebra

Ideal.finrank_quotient_eq_sum

∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsPrincipalIdealRing R] [inst_5 : IsDomain S] (F : Type u_4) [inst_6 : CommRing F] [inst_7 : Algebra F R]
  [inst_8 : Algebra F S] [IsScalarTower F R S] {I : Ideal S} (hI : I ≠ ⊥) {ι : Type u_5} [inst_10 : Fintype ι]
  (b : Module.Basis ι R S) [Nontrivial F] [∀ (i : ι), Module.Free F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})]
  [∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})],
  Module.finrank F (S ⧸ I) = ∑ i, Module.finrank F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})

Defined in

Mathlib.LinearAlgebra.FreeModule.IdealQuotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsPrincipalIdealRingIsDomainCommRingAlgebraAlgebraIsScalarTowerFintypeNontrivialModule.FreeModule.Finite