coe_prodMap' — Mathlib

English

The coercion of the product map equals the product of the coerced maps as a function.

Русский

Приведение к линейному отображению произведения равно произведению приведённых отображений как функция.

LaTeX

$$$\\uparrow(f_1.prodMap f_2) = \\prodMap(f_1,f_2)$$$

Lean4

@[simp, norm_cast]
theorem coe_prodMap' (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) : ⇑(f₁.prodMap f₂) = Prod.map f₁ f₂ :=
  rfl

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