coe_mul — Mathlib

English

The map f ↦ f, sending a locally constant function to its underlying function, preserves multiplication and identity; i.e., it is a monoid hom from LocallyConstant(X,Y) to X → Y.

Русский

Отображение f ↦ f, переводящее локально константную функцию в соответствующую обычную функцию, сохраняет умножение и единицу; то есть является гомоморфизмом моноида.

LaTeX

$$$\widehat{f * g} = \widehat{f} \cdot \widehat{g}$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mul [Mul Y] (f g : LocallyConstant X Y) : ⇑(f * g) = f * g :=
  rfl

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