instMulOneClass — Mathlib

English

If Y has a MulOneClass, then LocallyConstant(X,Y) inherits a MulOneClass structure, i.e., it is a monoid with unit given by the constant function 1.

Русский

Если у Y есть структуру MulOneClass, то LocallyConstant(X,Y) наследует структуру MulOneClass, то есть является моноидом с единицей, заданной константной функцией 1.

LaTeX

$$\text{LocallyConstant}(X,Y) \,\text{is a} \, MulOneClass \,\text{under pointwise operations}.$$

Lean4

@[to_additive]
instance [MulOneClass Y] : MulOneClass (LocallyConstant X Y) :=
  Function.Injective.mulOneClass DFunLike.coe DFunLike.coe_injective' rfl fun _ _ => rfl

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