localization_add — Mathlib

English

Localization respects addition: (r + s).localization L W = r.localization L W + s.localization L W.

Русский

Локализация сохраняет сложение: локализация суммы равна сумме локализаций.

LaTeX

$$$ (r + s).localization\; L\; W = r.localization\; L\; W + s.localization\; L\; W $$$

Lean4

theorem localization_add : (r + s).localization L W = r.localization L W + s.localization L W :=
  ext_of_localization L W _ _
    (fun X => by
      rw [localization_app, NatTrans.app_add, NatTrans.app_add, L.map_add, localization_app, localization_app])

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