coe_smul — Mathlib

English

The scalar action on LocallyConstant is compatible with the underlying function, i.e. the coe map commutes with smul: coe(r • f) = r • coe(f).

Русский

Слияние скаляра с локально константной функцией совместимо: coe(r • f) = r • coe(f).

LaTeX

$$$\operatorname{coe}(r \cdot f) = r \cdot \operatorname{coe}(f).$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_smul [SMul R Y] (r : R) (f : LocallyConstant X Y) : ⇑(r • f) = r • (f : X → Y) :=
  rfl

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