minOrder_le_natCard — Mathlib

English

If s is a nontrivial finite subgroup of G, then minOrder G ≤ Nat.card s.

Русский

Если s — ненулевающая конечная подгруппа G, то minOrder G ≤ Nat.card s.

LaTeX

$$$s \neq \bot \land (s:\,G).Finite \Rightarrow \minOrder(G) \le \operatorname{Nat.card}(s)$$$

Lean4

@[to_additive]
theorem minOrder_le_natCard (hs : s ≠ ⊥) (hs' : (s : Set G).Finite) : minOrder G ≤ Nat.card s :=
  le_minOrder_iff_forall_subgroup.1 le_rfl hs hs'

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