coe_neg — Mathlib

English

The coerced negation of a LieDerivation corresponds to the negation of its underlying linear map.

Русский

Приведение отрицания к LieDerivation соответствует отрицанию её базового линейного отображения.

LaTeX

$$$\text{Eq } (\text{instFunLike}.coe (\text{instNeg}.neg D)) = (\text{instHSub}.hSub (\text{LieModule}.bracket a (\text{instFunLike}.coe D b)) (\text{LieModule}.bracket b (\text{instFunLike}.coe D a)))$$$

Lean4

@[simp]
theorem coe_neg (D : LieDerivation R L M) : ⇑(-D) = -D :=
  rfl

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