prodMap_apply

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearMap.prodMap_apply

English

For any pair (m, n) ∈ M × M2, the map f.prodMap g sends (m, n) to (f(m), g(n)).

Русский

Для пары (m, n) ∈ M × M₂ отображение f.prodMap g отправляет (m, n) в (f(m), g(n)).

LaTeX

$$$ (f \\text{ prodMap } g)(m, n) = (f(m),\\, g(n)). $$$

Lean4

@[simp]
theorem prodMap_apply (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x) : f.prodMap g x = (f x.1, g x.2) :=
  rfl

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

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

Разделы

Аффилиация

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