mk'_neg

Mathlib.RingTheory.Localization.Defs

URI: https://scilib.ai/kg/mathlib#IsLocalization.mk'_neg

English

Negation commutes with mk' in localization: mk' S (−x) y = − mk' S x y.

Русский

Отражение через mk' в локализации коммутирует с отрицанием: mk' S (−x) y = − mk' S x y.

LaTeX

$$$\\mathrm{mk'}\\ S (-x) y = -\\mathrm{mk'}\\ S x y$$$

Lean4

theorem mk'_neg (x : R) (y : M) : mk' S (-x) y = -mk' S x y := by
  rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru