instNeg

Mathlib.RingTheory.Derivation.Basic

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

← MathLib Explorer

English

There is a canonical Neg instance for Derivation, defined via mk' with negated D.

Русский

Существует канонический экземпляр отрицания для Derivation, заданный через mk' от -D.

LaTeX

$$Derivation.instNeg : Neg (Derivation R A M)$$

Lean4

instance : Neg (Derivation R A M) :=
  ⟨fun D => mk' (-D) fun a b => by simp only [LinearMap.neg_apply, smul_neg, neg_add_rev, leibniz, coeFn_coe, add_comm]⟩

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

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

Разделы

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

Аффилиация

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