prodMap — Mathlib

English

Define the product map from M × N to M' × N' by composing with fst and snd: (f.prodMap g) = (f ∘ fst) × (g ∘ snd).

Русский

Определим произведение гомоморфизмов: (f × g) с использованием fst и snd: (f.prodMap g) = (f ∘ fst) × (g ∘ snd).

LaTeX

$$$\mathrm{prodMap}\,f\,g = (f \circ \mathrm{fst}) \;\mathrm{prod}\; (g \circ \mathrm{snd})$$$

Lean4

/-- `Prod.map` as a `MonoidHom`. -/
@[to_additive prodMap /-- `Prod.map` as an `AddMonoidHom` -/
    ]
def prodMap : M × N →ₙ* M' × N' :=
  (f.comp (fst M N)).prod (g.comp (snd M N))

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