add — Mathlib

English

The submodule p, viewed as an abstract additive structure, inherits addition from M by pointwise addition on representatives.

Русский

Подмодуль p, рассматриваемый как аддитивная структура, наследует сложение от M поко по представителям.

LaTeX

$$$ \\text{Add } p \\text{ is given by } (x,y)\\mapsto (x+y) \\\\text{ with } x,y\\in p$$$

Lean4

instance add : Add p :=
  ⟨fun x y => ⟨x.1 + y.1, add_mem x.2 y.2⟩⟩

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