mk_neg — Mathlib

English

For any m and s in the localized module, the fraction obtained by negating the numerator represents the negation of the localized element; i.e., mk(−m) s = − mk(m) s.

Русский

Для любого m и s в локализованном модуле дробь с отрицательным числителем представляет противоположный элемент локализации; то есть mk(−m) s = − mk(m) s.

LaTeX

$$$\\mathrm{mk}(-m, s) = -\\mathrm{mk}(m, s)$$$

Lean4

theorem mk_neg {M : Type*} [AddCommGroup M] [Module R M] {m : M} {s : S} : mk (-m) s = -mk m s :=
  rfl

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