prodMkLeft_add — Mathlib

English

prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η; the right-product kernel is additive in its base kernel.

Русский

Правая продукция по отношению к сумме ядер равна сумме правых произведений.

LaTeX

$$$ \operatorname{prodMkRight} γ (\kappa + \eta) = \operatorname{prodMkRight} γ \kappa + \operatorname{prodMkRight} γ \eta $$$

Lean4

@[simp]
theorem prodMkLeft_add (κ η : Kernel α β) : prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η := by ext; simp

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