English
The action of ZMod(2) on Additive(Units Int) is well-defined and respects the module axioms.
Русский
Действие ZMod(2) на Additive(Units Int) корректно и удовлетворяет аксиомам модуля.
LaTeX
$$$\text{Module} (ZMod(2)) (Additive(Units(Int))).$$$
Lean4
/-- This is an indirect way of saying that `ℤˣ` has a power operation by `ZMod 2`. -/
instance : Module (ZMod 2) (Additive ℤˣ)
where
smul z au := .ofMul <| au.toMul ^ z.val
one_smul _ := Additive.toMul.injective <| pow_one _
mul_smul z₁ z₂
au :=
Additive.toMul.injective <| by
dsimp only [ZMod.smul_units_def, toMul_nsmul]
rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]
smul_zero _ := Additive.toMul.injective <| one_pow _
smul_add _ _ _ := Additive.toMul.injective <| mul_pow _ _ _
add_smul z₁ z₂
au :=
Additive.toMul.injective <| by
dsimp only [ZMod.smul_units_def, toMul_nsmul, toMul_add]
rw [← pow_add, ZMod.val_add, ← Int.units_pow_eq_pow_mod_two]
zero_smul au := Additive.toMul.injective <| pow_zero au.toMul
