neg — Mathlib

English

Negation on Ore localization is defined via negation on the numerator.

Русский

Отрицание на локализации Оре задаётся через отрицание числителя.

LaTeX

$$Neg (X[S^{-1}]) is defined by $(r /ₒ s) \mapsto (-r) /ₒ s$$$

Lean4

/-- Negation on the Ore localization is defined via negation on the numerator. -/
@[irreducible]
protected def neg : X[S⁻¹] → X[S⁻¹] :=
  liftExpand (fun (r : X) (s : S) => -r /ₒ s) fun r t s ht => by
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed

    beta_reduce
    rw [← smul_neg, ← OreLocalization.expand]

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