prodMap — Mathlib

English

The map prodMap f g equals the product of the compositions with fst and snd: prodMap f g = (f ∘ fst).prod (g ∘ snd).

Русский

Отображение prodMap f g равно произведению композиций с fst и snd: prodMap f g = (f ∘ fst).prod (g ∘ snd).

LaTeX

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

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))

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