zmodEquivZPowers_symm_apply_pow — Mathlib

English

The inverse mapping sends Additive.ofMul(⟨ζ^i, i, rfl⟩) to i.

Русский

Обратное отображение отправляет Additive.ofMul(⟨ζ^i, i, rfl⟩) в i.

LaTeX

$$h.zmodEquivZPowers.symm (Additive.ofMul (⟨ζ^i, i, rfl⟩)) = i$$

Lean4

@[simp]
theorem zmodEquivZPowers_symm_apply_pow (i : ℕ) :
    h.zmodEquivZPowers.symm (Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ)) = i := by
  rw [← h.zmodEquivZPowers.symm_apply_apply i, zmodEquivZPowers_apply_coe_nat]

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