prod_fst_snd

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.prod_fst_snd

English

The backward direction of prodEquiv sends a morphism h: A→ₙₐ[R] B×C to (fst ∘ h, snd ∘ h).

Русский

Обратное направление prodEquiv отправляет гомоморфизм h: A→ₙₐ[R] B×C в (fst ∘ h, snd ∘ h).

LaTeX

$$$\text{invFun}(h)=(\text{fst} \circ h, \text{snd} \circ h)$$$

Lean4

@[simp]
theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
  coe_injective Pi.prod_fst_snd

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

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

Разделы

Аффилиация

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