natCast_smul_units — Mathlib

English

There is a canonical Module action of ZMod(2) on Additive(Units Int), consistent with addition and multiplication.

Русский

Существует каноническое действие модуля ZMod(2) на Additive(Units Int), согласованное с операциями сложения и умножения.

LaTeX

$$$\text{Module} (ZMod(2)) (Additive(Units(Int))).$$$

Lean4

theorem natCast_smul_units (n : ℕ) (au : Additive ℤˣ) : (n : ZMod 2) • au = n • au :=
  (Int.units_pow_eq_pow_mod_two au n).symm

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