English
Let G be cyclic of order n and M act on G distributively; for m ∈ M and g ∈ G, if φ(m) = k in ZMod n, then m • g = g^k.
Русский
Пусть G циклическая группа порядка n, и M действует на G дистрибутивно; для элемента m ∈ M и g ∈ G, если φ(m) = k по модулю n, то m • g = g^k.
LaTeX
$$$(\exists \phi: M \rightarrow^* \mathbb{Z}/n\mathbb{Z})\; \Rightarrow\; m \cdot g = g^{k}$, где $\phi(m) = k$$$
Lean4
theorem toMonoidHomZModOfIsCyclic_apply {M : Type*} [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ}
(hn : Nat.card G = n) (m : M) (g : G) (k : ℤ) (h : toMonoidHomZModOfIsCyclic G M hn m = k) : m • g = g ^ k :=
by
rw [← MulDistribMulAction.toMonoidHom_apply, (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec g,
zpow_eq_zpow_iff_modEq]
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard g))
rwa [hn, ← ZMod.intCast_eq_intCast_iff]
