instAdd — Mathlib

English

The set of continuous alternating maps carries an additive structure defined pointwise by addition of underlying maps.

Русский

Множество непрерывных чередующих отображений обладает аддитивной структурой, задаваемой по точкам сложением соответствующих отображений.

LaTeX

$$$ (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap $$$

Lean4

instance : Add (M [⋀^ι]→L[R] N) :=
  ⟨fun f g => ⟨f.1 + g.1, (f.toAlternatingMap + g.toAlternatingMap).map_eq_zero_of_eq⟩⟩

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