snd_prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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