prodMap — Mathlib

English

Given f: R →+* R' and g: S →+* S', define prodMap f g: R × S →+* R' × S' by prodMap f g = (f ∘ fst R S) × (g ∘ snd R S).

Русский

Задается отображение prodMap f g: R × S →+* R' × S' заданное как (f ∘ fst, g ∘ snd).

LaTeX

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

Lean4

/-- `Prod.map` as a `RingHom`. -/
def prodMap : R × S →+* R' × S' :=
  (f.comp (fst R S)).prod (g.comp (snd R S))

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