zmodEquivZPowers_apply_coe_nat — Mathlib

English

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

Русский

Для i ∈ N имеет место 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_nat (i : ℕ) :
    h.zmodEquivZPowers i = Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ) :=
  by
  have : (i : ZMod k) = (i : ℤ) := by norm_cast
  simp only [this, zmodEquivZPowers_apply_coe_int, zpow_natCast]

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