cardinalMk — Mathlib

English

Under the same hypotheses, the cardinality of the localization equals the base cardinality.

Русский

При тех же предпосылках кардинальность локализации равна кардинальности основания.

LaTeX

$$$\\#L = \\#R$$$

Lean4

/-- If you do not localize at any zero-divisors, localization preserves cardinality. -/
theorem cardinalMk (L : Type u) [CommRing L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] (hS : S ≤ R⁰) :
    #L = #R := by simpa using lift_cardinalMk L S hS

Похожие утверждения