English
The ZMod n-action on a substructure K satisfies the standard module axioms: linearity in the scalar and in the vector arguments, and identity action by 1, etc.
Русский
Действие ZMod n на подструктуру K удовлетворяет стандартным аксиомам модуля: линейность по скаляру и по векторам, равенство единице действия и т.д.
LaTeX
$$$\forall a,b \in \mathbb{Z}/n\mathbb{Z}, \forall x \in K:\ (a+b)\cdot x = a\cdot x + b\cdot x \wedge \forall a\in \mathbb{Z}/n\mathbb{Z}, \forall x,y\in K:\ a\cdot (x+y) = a\cdot x + a\cdot y$$$
Lean4
@[to_additive (attr := simp) nsmul_zmod_val_inv_nsmul]
theorem pow_zmod_val_inv_pow (hn : (Nat.card α).gcd n = 1) (a : α) : (a ^ (n⁻¹ : ZMod (Nat.card α)).val) ^ n = a :=
by
replace hn : (Nat.card α).Coprime n := hn
rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
