instNonAssocRing — Mathlib

English

If Y is a nonassociative ring, then LocallyConstant(X, Y) inherits a natural nonassociative ring structure via the same pointwise operations.

Русский

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

LaTeX

$$$\operatorname{NonAssocRing}(\operatorname{LocallyConstant}(X,Y))$$$

Lean4

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

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