instAdd — Mathlib

English

There is a canonical addition operation on locally finite within U functions, defined by lifting the pointwise sum of representatives that lie in the subgroup.

Русский

Существует каноническое сложение для функций внутри U, определяемое по покомпонентному сложению представителей из подгруппы.

LaTeX

$$Add instance on $\\text{locallyFinsuppWithin } U Y$ given by $D_1+D_2 = \\text{mk\_of\_mem}(D_1+D_2)$.$$

Lean4

instance [AddCommGroup Y] : Add (locallyFinsuppWithin U Y) where
  add D₁ D₂ := mk_of_mem (D₁ + D₂) <| add_mem D₁.memAddSubgroup D₂.memAddSubgroup

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