snd — Mathlib

English

The underlying function of the product of two StarAlgHom equals the product of their underlying functions.

Русский

Функция-основание произведения двух StarAlgHom равна произведению их функций-оснований.

LaTeX

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

Lean4

/-- The second projection of a product is a ⋆-algebra homomorphism. -/
@[simps!]
def snd : A × B →⋆ₐ[R] B :=
  { AlgHom.snd R A B with map_star' := fun _ => rfl }

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