orderOf_le_card — Mathlib

English

Let s be a finite subgroup of G and x ∈ s. Then the order of x is at most the cardinality of s.

Русский

Пусть s — конечная подгруппа G и x ∈ s. Тогда порядок x не превосходит кардинальность s.

LaTeX

$$$\operatorname{orderOf}(x) \le \operatorname{Nat.card}(s)$$$

Lean4

@[to_additive]
theorem orderOf_le_card {G : Type*} [Group G] (s : Subgroup G) (hs : (s : Set G).Finite) {x} (hx : x ∈ s) :
    orderOf x ≤ Nat.card s :=
  le_of_dvd (Nat.card_pos_iff.2 <| ⟨s.coe_nonempty.to_subtype, hs.to_subtype⟩) <| s.orderOf_dvd_natCard hx

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