prod — Mathlib

English

The Pi.prod of two morphisms is a morphism to the product, with the star structure preserved.

Русский

Pi.prod двух морфизмов является морфизмом в произведение, сохраняющим структуру звезды.

LaTeX

$$$ f : A \rightarrow⋆ₐ[R] B$, $g : A \rightarrow⋆ₐ[R] C$ ⇒ $ f.prod g : A \rightarrow⋆ₐ[R] B × C $$$

Lean4

/-- The `Pi.prod` of two morphisms is a morphism. -/
@[simps!]
def prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : A →⋆ₐ[R] B × C :=
  { f.toAlgHom.prod g.toAlgHom with map_star' := fun x => by simp [Prod.star_def, map_star] }

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