powEquiv' — Mathlib

English

If p is prime and p ∤ n, there is a powEquiv' bijection G ≃ G.

Русский

Если p — простое и p не делит n, существует биекция powEquiv' : G ≃ G.

LaTeX

$$$\IsPGroup(p,G) \rightarrow [\Fact(p.Prime)] \rightarrow \forall {n}, \; p \nmid n \rightarrow G \simeq G$$$

Lean4

/-- If `p ∤ n`, then the `n`th power map is a bijection. -/
noncomputable abbrev powEquiv' {n : ℕ} (hn : ¬p ∣ n) : G ≃ G :=
  powEquiv hG (hp.out.coprime_iff_not_dvd.mpr hn)

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