noncommCoprod_apply' — Mathlib

English

For the Pi-coproduct, (f.noncommCoprod g comm) applied to (m,n) equals g(n) f(m) (in that order).

Русский

Для копродукта по индексу Пи, (f.noncommCoprod g comm) applied to (m,n) равно g(n) f(m) (в указанном порядке).

LaTeX

$$$ (f.noncommCoprod g comm) (m,n) = g(n) \\cdot f(m). $$$

Lean4

/-- Variant of `MonoidHom.noncomCoprod_apply` with the product written in the other direction` -/
@[to_additive /-- Variant of `AddMonoidHom.noncomCoprod_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, MonoidHom.noncommCoprod_apply]

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