instNonUnitalNonAssocSemiring — Mathlib

English

LocallyConstant X Y forms a NonUnitalNonAssocSemiring with pointwise addition and multiplication when Y is a NonUnitalNonAssocSemiring.

Русский

LocallyConstant X Y образует NonUnitalNonAssocSemiring, если Y имеет такую же структуру точечно.

LaTeX

$$$\text{LocallyConstant}(X,Y)\text{ is a NonUnitalNonAssocSemiring with } (f+g)(x)=f(x)+g(x), (f\cdot g)(x)=f(x)g(x).$$$

Lean4

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

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