zmodEquivZPowers_apply_coe_int — Mathlib

English

For any integer i, h.zmodEquivZPowers i equals Additive.ofMul(⟨ζ^i, i, rfl⟩).

Русский

Для целого i имеет место равенство h.zmodEquivZPowers i = Additive.ofMul( ⟨ζ^i, i, rfl⟩ ).

LaTeX

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

Lean4

@[simp]
theorem zmodEquivZPowers_apply_coe_int (i : ℤ) :
    h.zmodEquivZPowers i = Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ) :=
  by
  rw [zmodEquivZPowers, AddEquiv.ofBijective_apply] -- Porting note: Original proof didn't have `rw`

  exact AddMonoidHom.liftOfRightInverse_comp_apply _ _ ZMod.intCast_rightInverse _ _

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