coe_prod — Mathlib

English

Let f: A →⋆ₙₐ[R] B and g: A →⋆ₙₐ[R] C be nonunital star algebra homomorphisms. Then the underlying function of the product map f.prod g equals the pointwise product of f and g, i.e. for all a ∈ A, (f.prod g)(a) = (f(a), g(a)).

Русский

Пусть f: A →⋆ₙₐ[R] B и g: A →⋆ₙₐ[R] C — неполные звёздно-алгебра-гомоморфизмы. Тогда отображение-произведение f.prod g является функцией-объектом, совпадающим с точечно-продуктовым отображением: для каждого a ∈ A имеет место (f.prod g)(a) = (f(a), g(a)).

LaTeX

$$$\\⇑(f.prod g) = \\Pi.prod f g$$$

Lean4

theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

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