instIsLeftCancelAdd — Mathlib

English

If M has a left-cancel property for addition, then the space of finitely supported functions ι →₀ M inherits the same left-cancel property.

Русский

Если M обладает свойством левого сжатия по сложению, то пространство ι →₀ M наследует это свойство.

LaTeX

$$$\\text{IsLeftCancelAdd}(M) \\Rightarrow \\text{IsLeftCancelAdd}(\\,\\iota \\to_{0} M\\,)$$$

Lean4

instance instIsLeftCancelAdd [IsLeftCancelAdd M] : IsLeftCancelAdd (ι →₀ M) where
  add_left_cancel _ _ _ h := ext fun x => add_left_cancel <| DFunLike.congr_fun h x

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