Documentation

Mathlib.Algebra.Ring.Pointwise.Finset

Pointwise operations of sets in a ring #

This file proves properties of pointwise operations of sets in a ring.

Tags #

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

source
def Finset.distribNeg {α : Type u_1} [DecidableEq α] [Mul α] [HasDistribNeg α] :
HasDistribNeg (Finset α)

Finset α has distributive negation if α has.

Equations
Instances For

    Note that Finset α is not a Distrib because s * t + s * u has cross terms that s * (t + u) lacks.

    -- {10, 16, 18, 20, 8, 9}
#eval {1, 2} * ({3, 4} + {5, 6} : Finset ℕ)

-- {10, 11, 12, 13, 14, 15, 16, 18, 20, 8, 9}
#eval ({1, 2} : Finset ℕ) * {3, 4} + {1, 2} * {5, 6}
    source
    theorem Finset.mul_add_subset {α : Type u_1} [DecidableEq α] [Distrib α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s * (t + u) ⊆ s * t + s * u
    source
    theorem Finset.add_mul_subset {α : Type u_1} [DecidableEq α] [Distrib α] (s : Finset α) (t : Finset α) (u : Finset α) :
    (s + t) * u ⊆ s * u + t * u
    source
    @[simp]
    theorem Finset.neg_smul_finset {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [DecidableEq β] {t : Finset β} {a : α} :
    -a • t = -(a • t)
    source
    @[simp]
    theorem Finset.neg_smul {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [DecidableEq β] {s : Finset α} {t : Finset β} [DecidableEq α] :
    -s • t = -(s • t)