instNeg

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.instNeg

English

There is a negation operation on polynomial laws giving a whole negation structure.

Русский

Существует операция отрицания над полиномальными законами, образующая структуру отрицания.

LaTeX

$$There is an instance $\Neg$ on $M \to_p_l[R] N$ defined by $f \mapsto -f$ with $(-f)^{toFun'}_S = - f^{toFun'}_S$.$$

Lean4

instance : Neg (M →ₚₗ[R] N) :=
  ⟨neg⟩

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

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

Разделы

Аффилиация

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