lift_cardinalMk — Mathlib

English

For a localization S of R with L, the lifted cardinalities are equal.

Русский

Для локализации S локализации R с L равны поднятые кардинальности.

LaTeX

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

Lean4

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

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