Theorems · Theorem · commutative algebra

IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace

∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  Submodule.spanFinrank (IsLocalRing.maximalIdeal R) =
    Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)

Defined in: Mathlib.Algebra.Module.SpanRankOperations
Cited by: 1 results in Mathlib
Foundations: Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsLocalRing IsNoetherianRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Module.finrankstatement · cited by 1,770
IsLocalRingstatement and proof · cited by 339
IsLocalRing.maximalIdealstatement and proof · cited by 297
IsNoetherianRingstatement and proof · cited by 268
IsLocalRing.ResidueFieldstatement · cited by 156
Submodule.spanFinrankstatement · cited by 49
IsLocalRing.CotangentSpacestatement · cited by 16
Ideal.fg_of_isNoetherianRingproof · cited by 9
IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fgproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

IsRegularLocalRing.iff_finrank_cotangentSpaceproof · cited by 0