coe_prodMap — Mathlib

English

The underlying AlgHom of f₁.prodMap f₂ equals the product of underlying AlgHoms: AlgHom from f₁.prodMap f₂ equals AlgHom from f₁ and f₂ composed separately.

Русский

Подлежащее AlgHom от f₁.prodMap f₂ равно произведению подлежащих AlgHom f₁ и f₂.

LaTeX

$$AlgHomClass.toAlgHom (f₁.prodMap f₂) = (AlgHomClass.toAlgHom f₁).prodMap (AlgHomClass.toAlgHom 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₂ : A × C →ₐ[R] B × D) = (f₁ : A →ₐ[R] B).prodMap (f₂ : C →ₐ[R] D) :=
  rfl

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