instIsLeftCancelAdd — Mathlib

English

If each β_i has left-cancellation under addition, then the function space Π₀ i, β_i also has left-cancellation under addition.

Русский

Если каждый β_i обладает левым устранением сложения, то пространство функций DFinsupp Π₀ i, β_i также обладает левым устранением.

LaTeX

$$$ (\forall i, IsLeftCancelAdd (β i)) \Rightarrow IsLeftCancelAdd (Π₀ i, β i) $$$

Lean4

instance instIsLeftCancelAdd [∀ i, AddZeroClass (β i)] [∀ i, IsLeftCancelAdd (β i)] : IsLeftCancelAdd (Π₀ i, β i) where
  add_left_cancel _ _ _ h := ext fun x => add_left_cancel <| DFunLike.congr_fun h x

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