instNeg — Mathlib

English

The negation of a left-invariant derivation is again a left-invariant derivation.

Русский

Отрицание лево-инвариантного выводителя снова является лево-инвариантным выводителем.

LaTeX

$$$ \forall X \in \mathrm{LeftInvariantDerivation}(I,G):\; -X \in \mathrm{LeftInvariantDerivation}(I,G). $$$

Lean4

instance : Neg (LeftInvariantDerivation I G) where neg X := ⟨-X, fun g => by simp [left_invariant']⟩

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