English
Under the same hypotheses as the noncommCoprod, the value of the coprod on a pair (m,n) is the product in the opposite order: (f.noncommCoprod g comm) (m,n) = g(n) f(m).
Русский
При тех же предположениях, что и для некоммутативного копродукта, значение копродукта на паре (m,n) равно произведению образов в обратном порядке: (f.noncommCoprod g comm)(m,n) = g(n) f(m).
LaTeX
$$$ (f.noncommCoprod\\, g\\, comm)\\, (m,n) = g(n) \\; f(m). $$$
Lean4
/-- Variant of `MulHom.noncommCoprod_apply` with the product written in the other direction` -/
@[to_additive /-- Variant of `AddHom.noncommCoprod_apply`, with the sum written in the other direction -/
]
theorem noncommCoprod_apply' (comm) (mn : M × N) : (f.noncommCoprod g comm) mn = g mn.2 * f mn.1 := by
rw [← comm, noncommCoprod_apply]
