Theorems · Theorem · commutative algebra

IsLocalRing.length_restrictScalars

∀ (A : Type u_1) (B : Type u_2) (M : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsLocalRing A]
  [inst_3 : IsLocalRing B] [inst_4 : Algebra A B] [inst_5 : IsLocalHom (algebraMap A B)] [inst_6 : AddCommGroup M]
  [inst_7 : Module A M] [inst_8 : Module B M] [IsScalarTower A B M],
  Module.length A M = Module.length B M * Module.length (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

If B/A is an extension of local rings, and if M is a B-module, then ℓ_A(M) = ℓ_B(M) * [κ(B) : κ(A)].

Defined in

Mathlib.RingTheory.LocalRing.Length

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingIsLocalRingIsLocalRingAlgebraIsLocalHomAddCommGroupModuleModuleIsScalarTower