neg

Mathlib.Algebra.Module.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#LinearEquiv.neg

English

There exists a linear equivalence representing negation on M, i.e., x ↦ -x.

Русский

Существует линейное эквивалентное отображение, задающее отрицание: x ↦ -x.

LaTeX

$$$\text{neg : } M \simeq_{R} M,\; x \mapsto -x$$$

Lean4

/-- `x ↦ -x` as a `LinearEquiv` -/
def neg : M ≃ₗ[R] M :=
  { Equiv.neg M, (-LinearMap.id : M →ₗ[R] M) with }

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

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

Разделы

Аффилиация

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