instIsRightCancelAdd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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