instAdd — Mathlib

English

There is a natural addition on HomogeneousLocalization 𝒜 x, defined by componentwise addition of representatives and passing to the quotient.

Русский

Существует естественное сложение на HomogeneousLocalization 𝒜 x, задаваемое покомпонентно через представителя и переход к эквивалентности по фактору.

LaTeX

$$There is an addition operation on $\mathrm{HomogeneousLocalization}_{\mathcal{A}}(x)$ defined by representatives.$$

Lean4

instance : Add (HomogeneousLocalization 𝒜 x) where
  add :=
    Quotient.map₂ (· + ·)
      fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) c3 c4
        (h' : Localization.mk _ _ = Localization.mk _ _) =>
      by
      change Localization.mk _ _ = Localization.mk _ _
      simp only [num_add, den_add]
      convert congr_arg₂ (· + ·) h h' <;> rw [Localization.add_mk] <;> rfl

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