zmodEquivZPowers — Mathlib

English

If 1 < k, then ζ^{k-1} = - sum_{i<k-1} ζ^i.

Русский

Если 1 < k, то ζ^{k-1} = - ∑_{i<k-1} ζ^i.

LaTeX

$$IsPrimitiveRoot(\\zeta, k) ∧ 1 < k ⟹ ζ^{k-1} = -\\sum_{i

Lean4

/-- The (additive) monoid equivalence between `ZMod k`
and the powers of a primitive root of unity `ζ`. -/
def zmodEquivZPowers (h : IsPrimitiveRoot ζ k) : ZMod k ≃+ Additive (Subgroup.zpowers ζ) :=
  AddEquiv.ofBijective
    (AddMonoidHom.liftOfRightInverse (Int.castAddHom <| ZMod k) _ ZMod.intCast_rightInverse
      ⟨{  toFun := fun i ↦ Additive.ofMul (⟨_, i, rfl⟩ : Subgroup.zpowers ζ)
          map_zero' := by simp only [zpow_zero]; rfl
          map_add' := by intro i j; simp only [zpow_add]; rfl }, fun i hi ↦
        by
        simp only [AddMonoidHom.mem_ker, CharP.intCast_eq_zero_iff (ZMod k) k, AddMonoidHom.coe_mk,
          Int.coe_castAddHom] at hi ⊢
        obtain ⟨i, rfl⟩ := hi
        simp [zpow_mul, h.pow_eq_one, one_zpow, zpow_natCast]⟩)
    (by
      constructor
      · rw [injective_iff_map_eq_zero]
        intro i hi
        rw [Subtype.ext_iff] at hi
        have := (h.zpow_eq_one_iff_dvd _).mp hi
        rw [← (CharP.intCast_eq_zero_iff (ZMod k) k _).mpr this, eq_comm]
        exact ZMod.intCast_rightInverse i
      · rintro ⟨ξ, i, rfl⟩
        refine ⟨Int.castAddHom (ZMod k) i, ?_⟩
        rw [AddMonoidHom.liftOfRightInverse_comp_apply]
        rfl)

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