prodMap_def

Mathlib.Algebra.Group.Prod

URI: https://scilib.ai/kg/mathlib#MulHom.prodMap_def

English

Equality definitional: prodMap f g equals (f ∘ fst).prod (g ∘ snd).

Русский

Определение: prodMap f g = (f ∘ fst).prod (g ∘ snd).

LaTeX

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

Lean4

@[to_additive prodMap_def]
theorem prodMap_def : prodMap f g = (f.comp (fst M N)).prod (g.comp (snd M N)) :=
  rfl

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

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

Разделы

Аффилиация

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