single_neg — Mathlib

English

For any m ∈ M and r ∈ R, the basis element with negated coefficient equals the negation of the basis element with the original coefficient: single m (-r) = - single m r.

Русский

Единичный элемент с отрицательным коэффициентом равен отрицанию единичного элемента с исходным коэффициентом: single m (-r) = - single m r.

LaTeX

$$$\\mathrm{single}(m, -r) = -\\mathrm{single}(m, r).$$$

Lean4

@[to_additive (dont_translate := R)]
theorem single_neg (m : M) (r : R) : single m (-r) = -single m r := by simp [single]

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