one_lt_card_iff_ne_bot

Mathlib.Algebra.Group.Subgroup.Finite

URI: https://scilib.ai/kg/mathlib#Subgroup.one_lt_card_iff_ne_bot

← MathLib Explorer

English

For finite H, 1 < card(H) if and only if H is not the bottom subgroup.

Русский

Для конечной H верно: 1 < |H| тогда и только тогда H ≠ ⊥.

LaTeX

$$$[\text{Finite } H] \; 1 < \operatorname{card}(H) \iff H \neq \bot$$$

Lean4

@[to_additive one_lt_card_iff_ne_bot]
theorem one_lt_card_iff_ne_bot [Finite H] : 1 < Nat.card H ↔ H ≠ ⊥ :=
  lt_iff_not_ge.trans H.card_le_one_iff_eq_bot.not

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

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

Разделы

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

Аффилиация

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