card_bot

Mathlib.Algebra.Group.Submonoid.Membership

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

← MathLib Explorer

English

The bottom submonoid has exactly one element, namely the identity.

Русский

Нижний подмоноид содержит ровно один элемент — единицу.

LaTeX

$$$\\\\operatorname{card}(\\\\bot \\\\ : Submonoid M) = 1$$$

Lean4

@[to_additive]
theorem card_bot {_ : Fintype (⊥ : Submonoid M)} : card (⊥ : Submonoid M) = 1 :=
  card_eq_one_iff.2 ⟨⟨(1 : M), Set.mem_singleton 1⟩, fun ⟨_y, hy⟩ => Subtype.eq <| mem_bot.1 hy⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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