instDistrib — Mathlib

English

LocallyConstant X Y is distributive over addition and multiplication pointwise: f · (g + h) = f·g + f·h and (f+g)·h = f·h + g·h.

Русский

LocallyConstant X Y распределяет по сложению и умножению точечно: f·(g+h) = f·g + f·h и (f+g)·h = f·h + g·h.

LaTeX

$$$f\cdot(g+h) = f\cdot g + f\cdot h\quad\text{and}\quad (f+h)\cdot h = f\cdot h + g\cdot h.$$$

Lean4

instance [Distrib Y] : Distrib (LocallyConstant X Y) :=
  Function.Injective.distrib DFunLike.coe DFunLike.coe_injective' (fun _ _ => rfl) fun _ _ => rfl

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