fst_prod_snd

Mathlib.GroupTheory.Coprod.Basic

URI: https://scilib.ai/kg/mathlib#Monoid.Coprod.fst_prod_snd

English

fst and snd together reproduce toProd: (fst).prod (snd) = toProd.

Русский

Совокупность fst и snd восстанавливает toProd: (fst).prod (snd) = toProd.

LaTeX

$$$\\\\mathrm{fst} \\\\mathrm{.} \\\\mathrm{prod} \\\\mathrm{ snd} = \\\\mathrm{toProd}.$$$

Lean4

@[to_additive (attr := simp) fst_prod_snd]
theorem fst_prod_snd : (fst : M ∗ N →* M).prod snd = toProd := by ext1 <;> rfl

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

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

Разделы

Аффилиация

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