instNeg — Mathlib

English

There is a natural additive inverse operation on HomogeneousLocalization 𝒜 x, making it an additive group under the quotient construction by negating representatives.

Русский

Существует естественное противоположное (аддитивное) действие на HomogeneousLocalization 𝒜 x, что обеспечивает структуру аддитивной группы через отрицание представителя.

LaTeX

$$There is a Neg instance on $\mathrm{HomogeneousLocalization}_{\mathcal{A}}(x)$ given by negating representatives.$$

Lean4

instance : Neg (HomogeneousLocalization 𝒜 x) where
  neg :=
    Quotient.map' Neg.neg fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) =>
      by
      change Localization.mk _ _ = Localization.mk _ _
      simp only [num_neg, den_neg, ← Localization.neg_mk]
      exact congr_arg Neg.neg h

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