instNeg — Mathlib

English

In the localized module LocalizedModule S M, the negation operation is defined by negating the numerator while keeping the denominator fixed; i.e., the additive inverse of m over s is (−m) over s.

Русский

В локализованном модуле LocalizedModule S M операция отрицания задаётся как отрицание числителя при фиксированном знаменателе; то есть противоположный по знаку элемент m/s равен (−m)/s.

LaTeX

$$$-\\frac{m}{s} = \\frac{-m}{s}$$$

Lean4

instance {M : Type*} [AddCommGroup M] [Module R M] : Neg (LocalizedModule S M) where
  neg
    p :=
    liftOn p (fun x => LocalizedModule.mk (-x.1) x.2) fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨u, hu⟩ =>
      by
      rw [mk_eq]
      exact ⟨u, by simpa⟩

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