intCast_apply

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.intCast_apply

English

For any integer z, the endomorphism z acts by z times the input: (z : End_R(N1)) m = z · m.

Русский

Для целого z эндоморфизм действует как умножение на z: (z : End_R(N1)) m = z · m.

LaTeX

$$$ (z : \mathrm{End}_R(N_1)) (m) = z \cdot m $$$

Lean4

/-- See also `Module.End.intCast_def`. -/
@[simp]
theorem intCast_apply (z : ℤ) (m : N₁) : (z : Module.End R N₁) m = z • m :=
  rfl

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

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

Разделы

Аффилиация

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