prod

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.prod

← MathLib Explorer

English

Applying prodMap to (p1, p3) yields (f p1, g p3).

Русский

Применение prodMap к (p1, p3) даёт (f(p1), g(p3)).

LaTeX

$$$\\mathrm{prodMap}(f,g)(p_1,p_3) = (f(p_1), g(p_3))$$$

Lean4

/-- The product of two affine maps is an affine map. -/
@[simps linear]
def prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : P1 →ᵃ[k] P2 × P3
    where
  toFun := Pi.prod f g
  linear := f.linear.prod g.linear
  map_vadd' := by simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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