instNeg — Mathlib

English

There is a negation operation making LieDerivation into a group under addition, with the negation defined componentwise.

Русский

Существует операция отрицания, делающая LieDerivation группой по сложению; отрицание определяется по компонентам.

LaTeX

$$instNeg : LieDerivation R L M → LieDerivation R L M$$

Lean4

instance instNeg : Neg (LieDerivation R L M) :=
  ⟨fun D =>
    mk (-D) fun a b => by
      simp only [LinearMap.neg_apply, coeFn_coe, apply_lie_eq_sub, neg_sub, lie_neg, sub_neg_eq_add, add_comm,
        ← sub_eq_add_neg]⟩

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