negFunc

Mathlib.ModelTheory.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Ring.negFunc

← MathLib Explorer

English

The unary negation operation on a ring is denoted by negFunc, i.e., negFunc(x) = −x.

Русский

Унарная операция отрицания в кольце обозначается negFunc: negFunc(x) = −x.

LaTeX

$$$$ \text{negFunc}(x) = -x. $$$$

Lean4

/-- `RingFunc.neg`, but with the defeq type `Language.ring.Functions 1` instead
of `RingFunc 1` -/
abbrev negFunc : Language.ring.Functions 1 :=
  neg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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