intCast_apply

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.intCast_apply

English

An integer z acts on M by z • m, and the corresponding linear map sends m to z • m.

Русский

Целое число z действует на M как z • m, и соответствующее линейное отображение отправляет m в z • m.

LaTeX

$$(↑z : M) m = z • m$$

Lean4

@[simp]
theorem intCast_apply [IsTopologicalAddGroup M] (z : ℤ) (m : M) : (↑z : M →L[R] M) m = z • m :=
  rfl

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

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

Разделы

Аффилиация

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