prodMap — Mathlib

English

ProdMap is an affine map from P1 × P3 to P2 × P4 with toFun = Prod.map f g and linear = f.linear.prodMap g.linear.

Русский

ProdMap есть аффинное отображение из P1 × P3 в P2 × P4 с toFun = Prod.map f g и линейной частью = f.linear.prodMap g.linear.

LaTeX

$$$\\mathrm{prodMap}(f,g) : P_1 \\times P_3 \\to^a_k P_2 \\times P_4$ с toFun = \\mathrm{Prod.map}(f,g) и linear = f.linear.prodMap g.linear$$$

Lean4

/-- `Prod.map` of two affine maps. -/
@[simps linear]
def prodMap (f : P1 →ᵃ[k] P2) (g : P3 →ᵃ[k] P4) : P1 × P3 →ᵃ[k] P2 × P4
    where
  toFun := Prod.map f g
  linear := f.linear.prodMap g.linear
  map_vadd' := by simp

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