orderOf_coprime — Mathlib

English

If p is a prime base of a p-group, then for any n with gcd(p, n) = 1, the order of any element is coprime to n.

Русский

Если p — простое и G — p-группа, то для любого n с gcd(p, n) = 1 порядок любого элемента взаимно прост с n.

LaTeX

$$$\IsPGroup(p,G) \rightarrow \forall n, \; p \text{Coprime } n \rightarrow \forall g \in G, \operatorname{order}(g) \text{ Coprime } n$$$

Lean4

theorem orderOf_coprime {n : ℕ} (hn : p.Coprime n) (g : G) : (orderOf g).Coprime n :=
  let ⟨k, hk⟩ := hG g
  (hn.pow_left k).coprime_dvd_left (orderOf_dvd_of_pow_eq_one hk)

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