instAdd — Mathlib

English

For any a ∈ Γ and r,s ∈ R, the single-a map is additive: single a (r+s) = single a r + single a s.

Русский

Для любого a, r, s: single a (r+s) = single a r + single a s.

LaTeX

$$$$ \operatorname{single}_a(r+s) = \operatorname{single}_a(r) + \operatorname{single}_a(s). $$$$

Lean4

instance : Add (HahnSeries Γ R) where
  add x
    y :=
    { coeff := x.coeff + y.coeff
      isPWO_support' := (x.isPWO_support.union y.isPWO_support).mono (Function.support_add _ _) }

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