orderOf_le_card — Mathlib

English

For a finite submonoid s of G and x ∈ s, the order of x is at most the cardinality of s.

Русский

Для конечного подмоноида s в G и x ∈ s, порядок x не превышает card(s).

LaTeX

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

Lean4

@[to_additive]
theorem orderOf_le_card {G : Type*} [Group G] (s : Submonoid G) (hs : (s : Set G).Finite) {x} (hx : x ∈ s) :
    orderOf x ≤ Nat.card s := by rw [← Nat.card_submonoidPowers]; exact Nat.card_mono hs <| powers_le.2 hx

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