mk_neg

Mathlib.LinearAlgebra.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.Quotient.mk_neg

English

Negation in the quotient is given by mk(−x) = −mk(x).

Русский

Отрицание в фактор-модуле задаётся как mk(−x) = −mk(x).

LaTeX

$$$\operatorname{mk}(-x) = -\operatorname{mk}(x).$$$

Lean4

@[simp]
theorem mk_neg : (mk (-x) : M ⧸ p) = -(mk x) :=
  rfl

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

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

Разделы

Аффилиация

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