cardinalMk_le — Mathlib

English

The cardinality of the Ore localization is at most the cardinality of the base monoid R: #(OreLocalization S R) ≤ #R.

Русский

Кардинал локализации Оре не превышает кардинал основанного моноида R.

LaTeX

$$$\\#(OreLocalization S R) \\le \\#R$$$

Lean4

@[to_additive]
theorem cardinalMk_le : #(OreLocalization S R) ≤ #R :=
  by
  convert ← cardinalMk_le_max S R
  simp_rw [lift_id, max_eq_right_iff, mk_subtype_le]
    -- TODO: remove the `Commute` assumption

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