orderOf_dvd_natCard — Mathlib

English

In a finite group G, for any subgroup s and any x ∈ s, the order of x divides the cardinality of s.

Русский

В конечной группе G для любой подгруппы H и любого x ∈ H выполняется: orderOf(x) делится card(H).

LaTeX

$$$\forall s : Subgroup(G), \; \forall x \in s,\; \operatorname{orderOf}(x) \mid \operatorname{Nat.card}(s)$$$

Lean4

@[to_additive]
nonrec theorem orderOf_dvd_natCard {G : Type*} [Group G] (s : Subgroup G) {x} (hx : x ∈ s) : orderOf x ∣ Nat.card s :=
  by simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)

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