intCast_def

Mathlib.Algebra.Module.End

URI: https://scilib.ai/kg/mathlib#AddMonoid.End.intCast_def

English

For z ∈ ℤ, the natural cast of z into AddMonoid.End M equals DistribMulAction.toAddMonoidEnd ℤ M z.

Русский

Для z ∈ ℤ натуральное преобразование z в End(M) равно DistribMulAction.toAddMonoidEnd ℤ M z.

LaTeX

$$$(z : \\mathbb{Z}) = \\text{toAddMonoidEnd } \\mathbb{Z} M\\, z$$$

Lean4

theorem intCast_def (z : ℤ) : (↑z : AddMonoid.End M) = DistribMulAction.toAddMonoidEnd ℤ M z :=
  rfl

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

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

Разделы

Аффилиация

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