coe_neg

Mathlib.Algebra.Module.Submodule.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.coe_neg

English

The embedding of -x in p to M equals -x in M.

Русский

Встраивание -x из p в M равно -x в M.

LaTeX

$$$(-x: p) = -x$$$

Lean4

protected theorem coe_neg (x : p) : ((-x : p) : M) = -x :=
  NegMemClass.coe_neg _

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

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

Разделы

Аффилиация

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