Theorems · Theorem · commutative algebra

IsLocalization.lift_cardinalMk

∀ {R : Type u} [inst : CommRing R] (L : Type v) [inst_1 : CommRing L] [inst_2 : Algebra R L] (S : Submonoid R)
  [IsLocalization S L],
  S ≤ nonZeroDivisors R → Cardinal.lift.{u, v} (Cardinal.mk L) = Cardinal.lift.{v, u} (Cardinal.mk R)

Defined in

Mathlib.RingTheory.Localization.Cardinality

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsLocalization