coe_prod — Mathlib

English

The underlying AlgHom of the cartesian product of two endomorphisms equals the algebra product of the underlying AlgHoms: (f₁.prod f₂) as AlgHom = f₁.AlgHom.prod f₂.AlgHom.

Русский

Подложное AlgHom произведения эндоморфизмов равно произведению подлежащих AlgHom.

LaTeX

$$AlgHomClass.toAlgHom (f₁.prod f₂) = (AlgHomClass.toAlgHom f₁).prod (AlgHomClass.toAlgHom f₂)$$

Lean4

@[simp, norm_cast]
theorem coe_prod (f₁ : A →A[R] B) (f₂ : A →A[R] C) : (f₁.prod f₂ : A →ₐ[R] B × C) = AlgHom.prod f₁ f₂ :=
  rfl

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