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
theorem Finset.zero_mem_smul_finset_iff {R : Type u_1} {M : Type u_3} [Semiring R] [IsDomain R] [AddCommMonoid M] [DecidableEq M] [Module R M] [Module.IsTorsionFree R M] {t : Finset M} {r : R} (hr : r ≠ 0) :
0 ∈ r • t ↔ 0 ∈ t
source
theorem Finset.zero_mem_smul_iff {R : Type u_1} {M : Type u_3} [Semiring R] [IsDomain R] [AddCommMonoid M] [DecidableEq M] [Module R M] [Module.IsTorsionFree R M] {s : Finset R} {t : Finset M} :
0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
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)