lift_cardinalMk_le — Mathlib

English

The cardinality of the target localization equals the cardinality of the base ring, up to the cardinal lifting.

Русский

Кардинальность целевой локализации равна кардинальности базового кольца, с учётом поднятия кардинала.

LaTeX

$$$\\operatorname{Cardinal.lift}\\#L = \\operatorname{Cardinal.lift}\\#R$$$

Lean4

theorem lift_cardinalMk_le (S : Submonoid R) [IsLocalization S L] : Cardinal.lift.{u} #L ≤ Cardinal.lift.{v} #R :=
  by
  have := Localization.cardinalMk_le S
  rwa [← lift_le.{v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

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