prod_contLinear — Mathlib

English

The product map of two affine maps is a map into the product space: f: P₁ →ᴬ[k] P₂ and g: P₃ →ᴬ[k] P₄ yield f.prodMap g: P₁ × P₃ →ᴬ[k] P₂ × P₄.

Русский

Произведение отображений в произведение: f: P₁ →ᴬ[k] P₂ и g: P₃ →ᴬ[k] P₄ дают f.prodMap g: P₁ × P₃ →ᴬ[k] P₂ × P₄.

LaTeX

$$$$f.prodMap g : P_1 \\times P_3 \\toᴬ[k] P_2 \\times P_4.$$$$

Lean4

@[simp]
theorem prod_contLinear (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : (f.prod g).contLinear = f.contLinear.prod g.contLinear :=
  rfl

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