coe_prodMap

Mathlib.Algebra.Ring.Prod

URI: https://scilib.ai/kg/mathlib#NonUnitalRingHom.coe_prodMap

English

prodMap f g is the same as the composition-based product map; i.e., f.prodMap g = (f ∘ fst) × (g ∘ snd).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coe_prodMap : ⇑(prodMap f g) = Prod.map f g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru