cardinalMk_le

Mathlib.GroupTheory.MonoidLocalization.Cardinality

URI: https://scilib.ai/kg/mathlib#Localization.cardinalMk_le

English

The cardinality of Localization S is bounded above by the cardinality of M: #(Localization S) ≤ #M.

Русский

М тепло: кардинал локализации S не превышает кардинала исходного моноида M: #(Localization S) ≤ #M.

LaTeX

$$$\\#(Localization S) \\le \\#M$$$

Lean4

@[to_additive]
theorem cardinalMk_le : #(Localization S) ≤ #M :=
  OreLocalization.cardinalMk_le S

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru