coe_prodMap' — Mathlib

English

The coercion of f₁.prodMap f₂ equals the standard Prod.map of f₁ and f₂.

Русский

Приведение к функции от f₁.prodMap f₂ равно стандартному Prod.map f₁ f₂.

LaTeX

$$⇑(f₁.prodMap f₂) = Prod.map f₁ f₂$$

Lean4

@[simp, norm_cast]
theorem coe_prodMap' {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
    ⇑(f₁.prodMap f₂) = Prod.map f₁ f₂ :=
  rfl

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