pow_gcd_card_eq_one_iff — Mathlib

English

For any x ∈ G and n ∈ Nat, x^n = 1 if and only if x^{gcd(n, card G)} = 1.

Русский

Для любого x ∈ G и n ∈ Nat верно: x^n = 1 тогда и только тогда, когда x^{gcd(n, card G)} = 1.

LaTeX

$$x^n = 1 \Leftrightarrow x^{\gcd(n, |G|)} = 1$$

Lean4

@[to_additive gcd_nsmul_card_eq_zero_iff]
theorem pow_gcd_card_eq_one_iff : x ^ n = 1 ↔ x ^ gcd n (Fintype.card G) = 1 :=
  ⟨fun h => pow_gcd_eq_one _ h <| pow_card_eq_one, fun h =>
    by
    let ⟨m, hm⟩ := gcd_dvd_left n (Fintype.card G)
    rw [hm, pow_mul, h, one_pow]⟩

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