Documentation

Mathlib.Algebra.Ring.Action.Pointwise.Finset

Pointwise actions on sets in a ring #

This file proves properties of pointwise actions on sets in a ring.

Tags #

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction

source
@[simp]
theorem Finset.neg_smul_finset {R : Type u_1} {G : Type u_2} [Ring R] [AddCommGroup G] [Module R G] [DecidableEq G] {t : Finset G} {a : R} :
-a • t = -(a • t)
source
@[simp]
theorem Finset.neg_smul {R : Type u_1} {G : Type u_2} [Ring R] [AddCommGroup G] [Module R G] [DecidableEq G] {s : Finset R} {t : Finset G} [DecidableEq R] :
-s • t = -(s • t)