neg_smul_finset — Mathlib

English

For a finite set t of a module over a ring, scaling by -a distributes over the negation: -a • t = -(a • t).

Русский

Для конечного множества t модуля над кольцом умножение на -a распределяется над отрицанием: -a • t = -(a • t).

LaTeX

$$$-a \\cdot t = -(a \\cdot t)$$$

Lean4

@[simp]
theorem neg_smul_finset : -a • t = -(a • t) := by
  simp only [← image_smul, ← image_neg_eq_neg, image_image, neg_smul, Function.comp_def]

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