instMonoidWithZero — Mathlib

English

The endomorphism monoid A →⋆ₙₐ[R] A carries a zero element making it a MonoidWithZero under composition.

Русский

Моноид эндоморфизмов имеет нулевой элемент, образованный для композиции.

LaTeX

$$MonoidWithZero(End(A)) with zero and composition satisfy zero_mul and mul_zero$$

Lean4

instance : MonoidWithZero (A →⋆ₙₐ[R] A) :=
  { inferInstanceAs (Monoid (A →⋆ₙₐ[R] A)),
    inferInstanceAs (Zero (A →⋆ₙₐ[R] A)) with
    zero_mul := fun _ => ext fun _ => rfl
    mul_zero := fun f => ext fun _ => map_zero f }

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