instSemiringEnd — Mathlib

English

For any object X, the endomorphisms End(X) form a ring under addition and composition.

Русский

Для любого объекта X множество концевых морфизмов End(X) образует кольцо под сложением и композицией.

LaTeX

$$$\operatorname{Semiring}(\operatorname{End}(X))$$$

Lean4

/-- This instance is split off from the `Ring (End X)` instance to speed up instance search. -/
instance {X : C} : Semiring (End X) :=
  { End.monoid with
    zero_mul := fun f => by dsimp [mul]; exact HasZeroMorphisms.comp_zero f _
    mul_zero := fun f => by dsimp [mul]; exact HasZeroMorphisms.zero_comp _ f
    left_distrib := fun f g h => Preadditive.add_comp X X X g h f
    right_distrib := fun f g h => Preadditive.comp_add X X X h f g }

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