fst_prod — Mathlib

English

Let f: A →⋆ₙₐ[R] B and g: A →⋆ₙₐ[R] C be nonunital star algebra homomorphisms. Then the composition of the first projection map fst with the product f.prod g returns f; i.e. fst ∘ (f.prod g) = f.

Русский

Пусть f: A →⋆ₙₐ[R] B и g: A →⋆ₙₐ[R] C — неполные звёздно-алгебра-гомоморфизмы. Тогда композиция fst с произведением f.prod g даёт f; то есть fst ∘ (f.prod g) = f.

LaTeX

$$$ (fst R B C) \circ (f.prod g) = f $$$

Lean4

@[simp]
theorem fst_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : (fst R B C).comp (prod f g) = f := by ext; rfl

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