ofFinsupp_neg — Mathlib

English

Negation on finsupp lifts to SkewMonoidAlgebra: the negation of a singleton corresponds to negating the coefficient.

Русский

Отрицание в finsupp переносится в SkewMonoidAlgebra: отрицание единичного элемента соответствует отрицанию коэффициента.

LaTeX

$$$$ (\langle -a \rangle) = -\langle a \rangle $$$$

Lean4

@[simp]
theorem ofFinsupp_neg {a} : (⟨-a⟩ : SkewMonoidAlgebra k G) = -⟨a⟩ :=
  show _ = neg _ by rw [neg_def]

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