instNonUnitalNonAssocRing — Mathlib

English

If Y is a NonUnitalNonAssocRing, LocallyConstant X Y inherits a NonUnitalNonAssocRing with pointwise addition and multiplication.

Русский

Если Y — кольцо без нуля и без ассоциативности, LocallyConstant X Y наследует такую структуру по точкам.

LaTeX

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

Lean4

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

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