instMul — Mathlib

English

If Y is a multiplicative structure, the set of locally constant maps LocallyConstant(X,Y) inherits a pointwise multiplication: (f * g)(x) = f(x) g(x).

Русский

Если Y обладает умножением, множество локально постоянных отображений LocallyConstant(X,Y) наследует умножение по месту: (f * g)(x) = f(x) g(x).

LaTeX

$$(f * g)(x) = f(x) g(x) for all x$$

Lean4

@[to_additive]
instance [Mul Y] : Mul (LocallyConstant X Y) where mul f g := ⟨f * g, f.isLocallyConstant.mul g.isLocallyConstant⟩

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