snd_prod

Mathlib.Algebra.Algebra.NonUnitalHom

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

English

The forward direction of prodEquiv sends (f,g) to f.prod g.

Русский

Направление вперёд эквивалентности prodEquiv отправляет (f,g) в f.prod g.

LaTeX

$$$\text{toFun}((f,g))=f.\mathrm{prod} g$$$

Lean4

@[simp]
theorem snd_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (snd R B C).comp (prod f g) = g := by rfl

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

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

Разделы

Аффилиация

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