eq_bot_iff_card

Mathlib.Algebra.Group.Submonoid.Membership

URI: https://scilib.ai/kg/mathlib#Submonoid.eq_bot_iff_card

English

For a submonoid S, S = ⊥ iff card S = 1.

Русский

Для подмоноида S верно: S = ⊥ тогда и только тогда, когда card S = 1.

LaTeX

$$$S = \\\\bot \\\\iff \\\\operatorname{card}(S) = 1$$$

Lean4

@[to_additive]
theorem eq_bot_iff_card : S = ⊥ ↔ card S = 1 :=
  ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq⟩

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

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

Разделы

Аффилиация

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