cardinalMk_le — Mathlib

English

The cardinality of a localization L is at most the cardinality of the base ring R.

Русский

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

LaTeX

$$$\\#L \\le \\#R$$$

Lean4

/-- A localization always has cardinality less than or equal to the base ring. -/
theorem cardinalMk_le {L : Type u} [CommSemiring L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] : #L ≤ #R := by
  simpa using lift_cardinalMk_le (L := L) S

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