powEquiv_symm_apply — Mathlib

English

The inverse style of powEquiv satisfies (powEquiv hn)^{-1}(g) = g^{(order g) gcdB n}.

Русский

Обратное отображение powEquiv hn задается как g^{(order g) gcdB n}.

LaTeX

$$$\IsPGroup(p,G) \rightarrow \forall {n}, \; p.Coprime n \rightarrow (\mathrm{powEquiv}(hn)).symm\; g = g^{(\operatorname{order}(g)).\gcdB n}$$$

Lean4

@[simp]
theorem powEquiv_symm_apply {n : ℕ} (hn : p.Coprime n) (g : G) : (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n := by
  rw [← Nat.card_zpowers]; rfl

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