neg_apply

Mathlib.RingTheory.Derivation.Basic

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

English

The negation of a derivation applied to an argument equals the negation of the derivation applied to the argument.

Русский

Отрицание вывода, применённое к элементу, равно отрицанию обычного применения вывода.

LaTeX

$$$(-D) a = -(D a)$$$

Lean4

theorem neg_apply : (-D) a = -D a :=
  rfl

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

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

Разделы

Аффилиация

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