smul_units_def

Mathlib.Data.ZMod.IntUnitsPower

URI: https://scilib.ai/kg/mathlib#ZMod.smul_units_def

English

There is a canonical module structure of ZMod(2) on Additive(Units ℤ).

Русский

Существует каноническая структура модуля ZMod(2) над Additive(Units ℤ).

LaTeX

$$$\text{Module} (ZMod(2)) (Additive(\mathbb{Z}^{\times})).$$$

Lean4

theorem smul_units_def (z : ZMod 2) (au : Additive ℤˣ) : z • au = z.val • au :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru