zmodEquivZPowers_symm_apply_zpow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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