coe_prodMap

Mathlib.Algebra.Ring.Prod

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

English

The underlying function of prodMap f g is exactly the product map of f and g: its action is x ↦ (f x, g x).

Русский

Вещественная функция prodMap f g совпадает с обычным декартовым отображением: x ↦ (f x, g x).

LaTeX

$$$ \\bigl( (\\mathrm{prodMap} f g) \\bigr) = \\mathrm{Prod.map} \\, f \, g. $$$

Lean4

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

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

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

Разделы

Аффилиация

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