mathlib3 documentation

data.finset.pointwise

Pointwise operations of finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines pointwise algebraic operations on finsets.

Main declarations #

For finsets s and t:

For α a semigroup/monoid, finset α is a semigroup/monoid. As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}. See note [pointwise nat action].

Implementation notes #

We put all instances in the locale pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp.

Tags #

finset multiplication, finset addition, pointwise addition, pointwise multiplication, pointwise subtraction

0/1 as finsets #

source
@[protected]
def finset.has_one {α : Type u_2} [has_one α] :
has_one (finset α)

The finset 1 : finset α is defined as {1} in locale pointwise.

Equations
source
@[protected]
def finset.has_zero {α : Type u_2} [has_zero α] :
has_zero (finset α)

The finset 0 : finset α is defined as {0} in locale pointwise.

Equations
source
@[simp]
theorem finset.mem_one {α : Type u_2} [has_one α] {a : α} :
a ∈ 1 ↔ a = 1
source
@[simp]
theorem finset.mem_zero {α : Type u_2} [has_zero α] {a : α} :
a ∈ 0 ↔ a = 0
source
@[simp, norm_cast]
theorem finset.coe_zero {α : Type u_2} [has_zero α] :
↑0 = 0
source
@[simp, norm_cast]
theorem finset.coe_one {α : Type u_2} [has_one α] :
↑1 = 1
source
@[simp]
theorem finset.zero_subset {α : Type u_2} [has_zero α] {s : finset α} :
0 ⊆ s ↔ 0 ∈ s
source
@[simp]
theorem finset.one_subset {α : Type u_2} [has_one α] {s : finset α} :
1 ⊆ s ↔ 1 ∈ s
source
theorem finset.singleton_one {α : Type u_2} [has_one α] :
{1} = 1
source
theorem finset.singleton_zero {α : Type u_2} [has_zero α] :
{0} = 0
source
theorem finset.one_mem_one {α : Type u_2} [has_one α] :
1 ∈ 1
source
theorem finset.zero_mem_zero {α : Type u_2} [has_zero α] :
0 ∈ 0
source
theorem finset.one_nonempty {α : Type u_2} [has_one α] :
1.nonempty
source
theorem finset.zero_nonempty {α : Type u_2} [has_zero α] :
0.nonempty
source
@[protected, simp]
theorem finset.map_zero {α : Type u_2} {β : Type u_3} [has_zero α] {f : α ↪ β} :
finset.map f 0 = {⇑f 0}
source
@[protected, simp]
theorem finset.map_one {α : Type u_2} {β : Type u_3} [has_one α] {f : α ↪ β} :
finset.map f 1 = {⇑f 1}
source
@[simp]
theorem finset.image_zero {α : Type u_2} {β : Type u_3} [has_zero α] [decidable_eq β] {f : α → β} :
finset.image f 0 = {f 0}
source
@[simp]
theorem finset.image_one {α : Type u_2} {β : Type u_3} [has_one α] [decidable_eq β] {f : α → β} :
finset.image f 1 = {f 1}
source
theorem finset.subset_one_iff_eq {α : Type u_2} [has_one α] {s : finset α} :
s ⊆ 1 ↔ s = ∅ ∨ s = 1
source
theorem finset.subset_zero_iff_eq {α : Type u_2} [has_zero α] {s : finset α} :
s ⊆ 0 ↔ s = ∅ ∨ s = 0
source
theorem finset.nonempty.subset_one_iff {α : Type u_2} [has_one α] {s : finset α} (h : s.nonempty) :
s ⊆ 1 ↔ s = 1
source
theorem finset.nonempty.subset_zero_iff {α : Type u_2} [has_zero α] {s : finset α} (h : s.nonempty) :
s ⊆ 0 ↔ s = 0
source
@[simp]
theorem finset.card_one {α : Type u_2} [has_one α] :
1.card = 1
source
@[simp]
theorem finset.card_zero {α : Type u_2} [has_zero α] :
0.card = 1
source
def finset.singleton_zero_hom {α : Type u_2} [has_zero α] :
zero_hom α (finset α)

The singleton operation as a zero_hom.

Equations
source
def finset.singleton_one_hom {α : Type u_2} [has_one α] :
one_hom α (finset α)

The singleton operation as a one_hom.

Equations
source
@[simp]
theorem finset.coe_singleton_zero_hom {α : Type u_2} [has_zero α] :
⇑finset.singleton_zero_hom = has_singleton.singleton
source
@[simp]
theorem finset.coe_singleton_one_hom {α : Type u_2} [has_one α] :
⇑finset.singleton_one_hom = has_singleton.singleton
source
@[simp]
theorem finset.singleton_zero_hom_apply {α : Type u_2} [has_zero α] (a : α) :
⇑finset.singleton_zero_hom a = {a}
source
@[simp]
theorem finset.singleton_one_hom_apply {α : Type u_2} [has_one α] (a : α) :
⇑finset.singleton_one_hom a = {a}
source
def finset.image_zero_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_zero α] [decidable_eq β] [has_zero β] [zero_hom_class F α β] (f : F) :
zero_hom (finset α) (finset β)

Lift a zero_hom to finset via image

Equations
source
@[simp]
theorem finset.image_zero_hom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_zero α] [decidable_eq β] [has_zero β] [zero_hom_class F α β] (f : F) (s : finset α) :
⇑(finset.image_zero_hom f) s = finset.image ⇑f s
source
@[simp]
theorem finset.image_one_hom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_one α] [decidable_eq β] [has_one β] [one_hom_class F α β] (f : F) (s : finset α) :
⇑(finset.image_one_hom f) s = finset.image ⇑f s
source
def finset.image_one_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_one α] [decidable_eq β] [has_one β] [one_hom_class F α β] (f : F) :
one_hom (finset α) (finset β)

Lift a one_hom to finset via image.

Equations

Finset negation/inversion #

source
@[protected]
def finset.has_inv {α : Type u_2} [decidable_eq α] [has_inv α] :
has_inv (finset α)

The pointwise inversion of finset s⁻¹ is defined as {x⁻¹ | x ∈ s} in locale pointwise.

Equations
source
@[protected]
def finset.has_neg {α : Type u_2} [decidable_eq α] [has_neg α] :
has_neg (finset α)

The pointwise negation of finset -s is defined as {-x | x ∈ s} in locale pointwise.

Equations
source
theorem finset.inv_def {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
s⁻¹ = finset.image (λ (x : α), x⁻¹) s
source
theorem finset.neg_def {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
-s = finset.image (λ (x : α), -x) s
source
theorem finset.image_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
finset.image (λ (x : α), x⁻¹) s = s⁻¹
source
theorem finset.image_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
finset.image (λ (x : α), -x) s = -s
source
theorem finset.mem_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} {x : α} :
x ∈ -s ↔ ∃ (y : α) (H : y ∈ s), -y = x
source
theorem finset.mem_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} {x : α} :
x ∈ s⁻¹ ↔ ∃ (y : α) (H : y ∈ s), y⁻¹ = x
source
theorem finset.neg_mem_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} {a : α} (ha : a ∈ s) :
-a ∈ -s
source
theorem finset.inv_mem_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} {a : α} (ha : a ∈ s) :
a⁻¹ ∈ s⁻¹
source
theorem finset.card_inv_le {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
s⁻¹.card ≤ s.card
source
theorem finset.card_neg_le {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
(-s).card ≤ s.card
source
@[simp]
theorem finset.inv_empty {α : Type u_2} [decidable_eq α] [has_inv α] :
∅⁻¹ = ∅
source
@[simp]
theorem finset.neg_empty {α : Type u_2} [decidable_eq α] [has_neg α] :
-∅ = ∅
source
@[simp]
theorem finset.neg_nonempty_iff {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
(-s).nonempty ↔ s.nonempty
source
@[simp]
theorem finset.inv_nonempty_iff {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
s⁻¹.nonempty ↔ s.nonempty
source
theorem finset.nonempty.of_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
s⁻¹.nonempty → s.nonempty

Alias of the forward direction of finset.inv_nonempty_iff.

source
theorem finset.nonempty.inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
s.nonempty → s⁻¹.nonempty

Alias of the reverse direction of finset.inv_nonempty_iff.

source
theorem finset.nonempty.neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
s.nonempty → (-s).nonempty

Alias of the reverse direction of finset.inv_nonempty_iff.

source
theorem finset.nonempty.of_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
(-s).nonempty → s.nonempty

Alias of the forward direction of finset.inv_nonempty_iff.

source
theorem finset.inv_subset_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s t : finset α} (h : s ⊆ t) :
s⁻¹ ⊆ t⁻¹
source
theorem finset.neg_subset_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s t : finset α} (h : s ⊆ t) :
-s ⊆ -t
source
@[simp]
theorem finset.inv_singleton {α : Type u_2} [decidable_eq α] [has_inv α] (a : α) :
{a}⁻¹ = {a⁻¹}
source
@[simp]
theorem finset.neg_singleton {α : Type u_2} [decidable_eq α] [has_neg α] (a : α) :
-{a} = {-a}
source
@[simp]
theorem finset.inv_insert {α : Type u_2} [decidable_eq α] [has_inv α] (a : α) (s : finset α) :
(has_insert.insert a s)⁻¹ = has_insert.insert a⁻¹ s⁻¹
source
@[simp]
theorem finset.neg_insert {α : Type u_2} [decidable_eq α] [has_neg α] (a : α) (s : finset α) :
-has_insert.insert a s = has_insert.insert (-a) (-s)
source
@[simp, norm_cast]
theorem finset.coe_neg {α : Type u_2} [decidable_eq α] [has_involutive_neg α] (s : finset α) :
↑-s = -↑s
source
@[simp, norm_cast]
theorem finset.coe_inv {α : Type u_2} [decidable_eq α] [has_involutive_inv α] (s : finset α) :
↑s⁻¹ = (↑s)⁻¹
source
@[simp]
theorem finset.card_inv {α : Type u_2} [decidable_eq α] [has_involutive_inv α] (s : finset α) :
s⁻¹.card = s.card
source
@[simp]
theorem finset.card_neg {α : Type u_2} [decidable_eq α] [has_involutive_neg α] (s : finset α) :
(-s).card = s.card
source
@[simp]
theorem finset.preimage_neg {α : Type u_2} [decidable_eq α] [has_involutive_neg α] (s : finset α) :
s.preimage has_neg.neg _ = -s
source
@[simp]
theorem finset.preimage_inv {α : Type u_2} [decidable_eq α] [has_involutive_inv α] (s : finset α) :
s.preimage has_inv.inv _ = s⁻¹

Finset addition/multiplication #

source
@[protected]
def finset.has_add {α : Type u_2} [decidable_eq α] [has_add α] :
has_add (finset α)

The pointwise addition of finsets s + t is defined as {x + y | x ∈ s, y ∈ t} in locale pointwise.

Equations
source
@[protected]
def finset.has_mul {α : Type u_2} [decidable_eq α] [has_mul α] :
has_mul (finset α)

The pointwise multiplication of finsets s * t and t is defined as {x * y | x ∈ s, y ∈ t} in locale pointwise.

Equations
source
theorem finset.add_def {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
s + t = finset.image (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)
source
theorem finset.mul_def {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
s * t = finset.image (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)
source
theorem finset.image_mul_product {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst * x.snd) (s ×ˢ t) = s * t
source
theorem finset.image_add_product {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst + x.snd) (s ×ˢ t) = s + t
source
theorem finset.mem_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} {x : α} :
x ∈ s * t ↔ ∃ (y z : α), y ∈ s ∧ z ∈ t ∧ y * z = x
source
theorem finset.mem_add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} {x : α} :
x ∈ s + t ↔ ∃ (y z : α), y ∈ s ∧ z ∈ t ∧ y + z = x
source
@[simp, norm_cast]
theorem finset.coe_add {α : Type u_2} [decidable_eq α] [has_add α] (s t : finset α) :
↑(s + t) = ↑s + ↑t
source
@[simp, norm_cast]
theorem finset.coe_mul {α : Type u_2} [decidable_eq α] [has_mul α] (s t : finset α) :
↑(s * t) = ↑s * ↑t
source
theorem finset.mul_mem_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} {a b : α} :
a ∈ s → b ∈ t → a * b ∈ s * t
source
theorem finset.add_mem_add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} {a b : α} :
a ∈ s → b ∈ t → a + b ∈ s + t
source
theorem finset.card_add_le {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).card ≤ s.card * t.card
source
theorem finset.card_mul_le {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).card ≤ s.card * t.card
source
theorem finset.card_mul_iff {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).card = s.card * t.card ↔ set.inj_on (λ (p : α × α), p.fst * p.snd) (↑s ×ˢ ↑t)
source
theorem finset.card_add_iff {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).card = s.card * t.card ↔ set.inj_on (λ (p : α × α), p.fst + p.snd) (↑s ×ˢ ↑t)
source
@[simp]
theorem finset.empty_mul {α : Type u_2} [decidable_eq α] [has_mul α] (s : finset α) :
∅ * s = ∅
source
@[simp]
theorem finset.empty_add {α : Type u_2} [decidable_eq α] [has_add α] (s : finset α) :
∅ + s = ∅
source
@[simp]
theorem finset.add_empty {α : Type u_2} [decidable_eq α] [has_add α] (s : finset α) :
s + ∅ = ∅
source
@[simp]
theorem finset.mul_empty {α : Type u_2} [decidable_eq α] [has_mul α] (s : finset α) :
s * ∅ = ∅
source
@[simp]
theorem finset.mul_eq_empty {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
s * t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.add_eq_empty {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
s + t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.add_nonempty {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[simp]
theorem finset.mul_nonempty {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem finset.nonempty.mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
s.nonempty → t.nonempty → (s * t).nonempty
source
theorem finset.nonempty.add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
s.nonempty → t.nonempty → (s + t).nonempty
source
theorem finset.nonempty.of_mul_left {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).nonempty → s.nonempty
source
theorem finset.nonempty.of_add_left {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).nonempty → s.nonempty
source
theorem finset.nonempty.of_add_right {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).nonempty → t.nonempty
source
theorem finset.nonempty.of_mul_right {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).nonempty → t.nonempty
source
theorem finset.mul_singleton {α : Type u_2} [decidable_eq α] [has_mul α] {s : finset α} (a : α) :
s * {a} = finset.image (λ (_x : α), _x * a) s
source
theorem finset.add_singleton {α : Type u_2} [decidable_eq α] [has_add α] {s : finset α} (a : α) :
s + {a} = finset.image (λ (_x : α), _x + a) s
source
theorem finset.singleton_add {α : Type u_2} [decidable_eq α] [has_add α] {s : finset α} (a : α) :
{a} + s = finset.image (has_add.add a) s
source
theorem finset.singleton_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s : finset α} (a : α) :
{a} * s = finset.image (has_mul.mul a) s
source
@[simp]
theorem finset.singleton_add_singleton {α : Type u_2} [decidable_eq α] [has_add α] (a b : α) :
{a} + {b} = {a + b}
source
@[simp]
theorem finset.singleton_mul_singleton {α : Type u_2} [decidable_eq α] [has_mul α] (a b : α) :
{a} * {b} = {a * b}
source
theorem finset.add_subset_add {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ + t₁ ⊆ s₂ + t₂
source
theorem finset.mul_subset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ * t₁ ⊆ s₂ * t₂
source
theorem finset.add_subset_add_left {α : Type u_2} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} :
t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂
source
theorem finset.mul_subset_mul_left {α : Type u_2} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} :
t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂
source
theorem finset.add_subset_add_right {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} :
s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t
source
theorem finset.mul_subset_mul_right {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} :
s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t
source
theorem finset.add_subset_iff {α : Type u_2} [decidable_eq α] [has_add α] {s t u : finset α} :
s + t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x + y ∈ u
source
theorem finset.mul_subset_iff {α : Type u_2} [decidable_eq α] [has_mul α] {s t u : finset α} :
s * t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x * y ∈ u
source
theorem finset.union_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} :
(s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t
source
theorem finset.union_add {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} :
s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)
source
theorem finset.add_union {α : Type u_2} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} :
s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)
source
theorem finset.mul_union {α : Type u_2} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} :
s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂
source
theorem finset.inter_mul_subset {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} :
s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)
source
theorem finset.inter_add_subset {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} :
s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)
source
theorem finset.add_inter_subset {α : Type u_2} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} :
s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)
source
theorem finset.mul_inter_subset {α : Type u_2} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} :
s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)
source
theorem finset.inter_mul_union_subset_union {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
source
theorem finset.inter_add_union_subset_union {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)
source
theorem finset.union_mul_inter_subset_union {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t₁ t₂ : finset α} :
(s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
source
theorem finset.union_add_inter_subset_union {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)
source
theorem finset.subset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {u : finset α} {s t : set α} :
↑u ⊆ s * t → (∃ (s' t' : finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t')

If a finset u is contained in the product of two sets s * t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' * t'.

source
theorem finset.subset_add {α : Type u_2} [decidable_eq α] [has_add α] {u : finset α} {s t : set α} :
↑u ⊆ s + t → (∃ (s' t' : finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' + t')

If a finset u is contained in the sum of two sets s + t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' + t'.

source
theorem finset.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_add α] [has_add β] [add_hom_class F α β] (f : F) {s t : finset α} :
finset.image ⇑f (s + t) = finset.image ⇑f s + finset.image ⇑f t
source
theorem finset.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_mul α] [has_mul β] [mul_hom_class F α β] (f : F) {s t : finset α} :
finset.image ⇑f (s * t) = finset.image ⇑f s * finset.image ⇑f t
source
def finset.singleton_add_hom {α : Type u_2} [decidable_eq α] [has_add α] :
add_hom α (finset α)

The singleton operation as an add_hom.

Equations
source
def finset.singleton_mul_hom {α : Type u_2} [decidable_eq α] [has_mul α] :
α →ₙ* finset α

The singleton operation as a mul_hom.

Equations
source
@[simp]
theorem finset.coe_singleton_add_hom {α : Type u_2} [decidable_eq α] [has_add α] :
⇑finset.singleton_add_hom = has_singleton.singleton
source
@[simp]
theorem finset.coe_singleton_mul_hom {α : Type u_2} [decidable_eq α] [has_mul α] :
⇑finset.singleton_mul_hom = has_singleton.singleton
source
@[simp]
theorem finset.singleton_mul_hom_apply {α : Type u_2} [decidable_eq α] [has_mul α] (a : α) :
⇑finset.singleton_mul_hom a = {a}
source
@[simp]
theorem finset.singleton_add_hom_apply {α : Type u_2} [decidable_eq α] [has_add α] (a : α) :
⇑finset.singleton_add_hom a = {a}
source
@[simp]
theorem finset.image_add_hom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_add α] [has_add β] [add_hom_class F α β] (f : F) (s : finset α) :
⇑(finset.image_add_hom f) s = finset.image ⇑f s
source
def finset.image_add_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_add α] [has_add β] [add_hom_class F α β] (f : F) :
add_hom (finset α) (finset β)

Lift an add_hom to finset via image

Equations
source
def finset.image_mul_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_mul α] [has_mul β] [mul_hom_class F α β] (f : F) :
finset α →ₙ* finset β

Lift a mul_hom to finset via image.

Equations
source
@[simp]
theorem finset.image_mul_hom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_mul α] [has_mul β] [mul_hom_class F α β] (f : F) (s : finset α) :
⇑(finset.image_mul_hom f) s = finset.image ⇑f s

Finset subtraction/division #

source
@[protected]
def finset.has_sub {α : Type u_2} [decidable_eq α] [has_sub α] :
has_sub (finset α)

The pointwise subtraction of finsets s - t is defined as {x - y | x ∈ s, y ∈ t} in locale pointwise.

Equations
source
@[protected]
def finset.has_div {α : Type u_2} [decidable_eq α] [has_div α] :
has_div (finset α)

The pointwise division of sfinets s / t is defined as {x / y | x ∈ s, y ∈ t} in locale pointwise.

Equations
source
theorem finset.div_def {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
s / t = finset.image (λ (p : α × α), p.fst / p.snd) (s ×ˢ t)
source
theorem finset.sub_def {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
s - t = finset.image (λ (p : α × α), p.fst - p.snd) (s ×ˢ t)
source
theorem finset.image_div_prod {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst / x.snd) (s ×ˢ t) = s / t
source
theorem finset.add_image_prod {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst - x.snd) (s ×ˢ t) = s - t
source
theorem finset.mem_div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} {a : α} :
a ∈ s / t ↔ ∃ (b c : α), b ∈ s ∧ c ∈ t ∧ b / c = a
source
theorem finset.mem_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} {a : α} :
a ∈ s - t ↔ ∃ (b c : α), b ∈ s ∧ c ∈ t ∧ b - c = a
source
@[simp, norm_cast]
theorem finset.coe_sub {α : Type u_2} [decidable_eq α] [has_sub α] (s t : finset α) :
↑(s - t) = ↑s - ↑t
source
@[simp, norm_cast]
theorem finset.coe_div {α : Type u_2} [decidable_eq α] [has_div α] (s t : finset α) :
↑(s / t) = ↑s / ↑t
source
theorem finset.div_mem_div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} {a b : α} :
a ∈ s → b ∈ t → a / b ∈ s / t
source
theorem finset.sub_mem_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} {a b : α} :
a ∈ s → b ∈ t → a - b ∈ s - t
source
theorem finset.sub_card_le {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).card ≤ s.card * t.card
source
theorem finset.div_card_le {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).card ≤ s.card * t.card
source
@[simp]
theorem finset.empty_sub {α : Type u_2} [decidable_eq α] [has_sub α] (s : finset α) :
∅ - s = ∅
source
@[simp]
theorem finset.empty_div {α : Type u_2} [decidable_eq α] [has_div α] (s : finset α) :
∅ / s = ∅
source
@[simp]
theorem finset.div_empty {α : Type u_2} [decidable_eq α] [has_div α] (s : finset α) :
s / ∅ = ∅
source
@[simp]
theorem finset.sub_empty {α : Type u_2} [decidable_eq α] [has_sub α] (s : finset α) :
s - ∅ = ∅
source
@[simp]
theorem finset.div_eq_empty {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
s / t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.sub_eq_empty {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
s - t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.sub_nonempty {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[simp]
theorem finset.div_nonempty {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem finset.nonempty.div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
s.nonempty → t.nonempty → (s / t).nonempty
source
theorem finset.nonempty.sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
s.nonempty → t.nonempty → (s - t).nonempty
source
theorem finset.nonempty.of_sub_left {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).nonempty → s.nonempty
source
theorem finset.nonempty.of_div_left {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).nonempty → s.nonempty
source
theorem finset.nonempty.of_div_right {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).nonempty → t.nonempty
source
theorem finset.nonempty.of_sub_right {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).nonempty → t.nonempty
source
@[simp]
theorem finset.sub_singleton {α : Type u_2} [decidable_eq α] [has_sub α] {s : finset α} (a : α) :
s - {a} = finset.image (λ (_x : α), _x - a) s
source
@[simp]
theorem finset.div_singleton {α : Type u_2} [decidable_eq α] [has_div α] {s : finset α} (a : α) :
s / {a} = finset.image (λ (_x : α), _x / a) s
source
@[simp]
theorem finset.singleton_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s : finset α} (a : α) :
{a} - s = finset.image (has_sub.sub a) s
source
@[simp]
theorem finset.singleton_div {α : Type u_2} [decidable_eq α] [has_div α] {s : finset α} (a : α) :
{a} / s = finset.image (has_div.div a) s
source
@[simp]
theorem finset.singleton_sub_singleton {α : Type u_2} [decidable_eq α] [has_sub α] (a b : α) :
{a} - {b} = {a - b}
source
@[simp]
theorem finset.singleton_div_singleton {α : Type u_2} [decidable_eq α] [has_div α] (a b : α) :
{a} / {b} = {a / b}
source
theorem finset.div_subset_div {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ / t₁ ⊆ s₂ / t₂
source
theorem finset.sub_subset_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ - t₁ ⊆ s₂ - t₂
source
theorem finset.sub_subset_sub_left {α : Type u_2} [decidable_eq α] [has_sub α] {s t₁ t₂ : finset α} :
t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂
source
theorem finset.div_subset_div_left {α : Type u_2} [decidable_eq α] [has_div α] {s t₁ t₂ : finset α} :
t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂
source
theorem finset.div_subset_div_right {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t : finset α} :
s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t
source
theorem finset.sub_subset_sub_right {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t : finset α} :
s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t
source
theorem finset.div_subset_iff {α : Type u_2} [decidable_eq α] [has_div α] {s t u : finset α} :
s / t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x / y ∈ u
source
theorem finset.sub_subset_iff {α : Type u_2} [decidable_eq α] [has_sub α] {s t u : finset α} :
s - t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x - y ∈ u
source
theorem finset.union_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t : finset α} :
s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)
source
theorem finset.union_div {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t : finset α} :
(s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t
source
theorem finset.sub_union {α : Type u_2} [decidable_eq α] [has_sub α] {s t₁ t₂ : finset α} :
s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)
source
theorem finset.div_union {α : Type u_2} [decidable_eq α] [has_div α] {s t₁ t₂ : finset α} :
s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂
source
theorem finset.inter_sub_subset {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t : finset α} :
s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)
source
theorem finset.inter_div_subset {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t : finset α} :
s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)
source
theorem finset.div_inter_subset {α : Type u_2} [decidable_eq α] [has_div α] {s t₁ t₂ : finset α} :
s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)
source
theorem finset.sub_inter_subset {α : Type u_2} [decidable_eq α] [has_sub α] {s t₁ t₂ : finset α} :
s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)
source
theorem finset.inter_div_union_subset_union {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
source
theorem finset.inter_sub_union_subset_union {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)
source
theorem finset.union_sub_inter_subset_union {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)
source
theorem finset.union_div_inter_subset_union {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t₁ t₂ : finset α} :
(s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
source
theorem finset.subset_sub {α : Type u_2} [decidable_eq α] [has_sub α] {u : finset α} {s t : set α} :
↑u ⊆ s - t → (∃ (s' t' : finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' - t')

If a finset u is contained in the sum of two sets s - t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' - t'.

source
theorem finset.subset_div {α : Type u_2} [decidable_eq α] [has_div α] {u : finset α} {s t : set α} :
↑u ⊆ s / t → (∃ (s' t' : finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t')

If a finset u is contained in the product of two sets s / t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' / t'.

Instances #

source
@[protected]
def finset.has_nsmul {α : Type u_2} [decidable_eq α] [has_zero α] [has_add α] :
has_smul ℕ (finset α)

Repeated pointwise addition (not the same as pointwise repeated addition!) of a finset. See note [pointwise nat action].

Equations
source
@[protected]
def finset.has_npow {α : Type u_2} [decidable_eq α] [has_one α] [has_mul α] :
has_pow (finset α) ℕ

Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a finset. See note [pointwise nat action].

Equations
source
@[protected]
def finset.has_zsmul {α : Type u_2} [decidable_eq α] [has_zero α] [has_add α] [has_neg α] :
has_smul ℤ (finset α)

Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a finset. See note [pointwise nat action].

Equations
source
@[protected]
def finset.has_zpow {α : Type u_2} [decidable_eq α] [has_one α] [has_mul α] [has_inv α] :
has_pow (finset α) ℤ

Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a finset. See note [pointwise nat action].

Equations
source
@[protected]
def finset.semigroup {α : Type u_2} [decidable_eq α] [semigroup α] :
semigroup (finset α)

finset α is a semigroup under pointwise operations if α is.

Equations
source
@[protected]
def finset.add_semigroup {α : Type u_2} [decidable_eq α] [add_semigroup α] :
add_semigroup (finset α)

finset α is an add_semigroup under pointwise operations if α is.

Equations
source
@[protected]
def finset.add_comm_semigroup {α : Type u_2} [decidable_eq α] [add_comm_semigroup α] :
add_comm_semigroup (finset α)

finset α is an add_comm_semigroup under pointwise operations if α is.

Equations
source
@[protected]
def finset.comm_semigroup {α : Type u_2} [decidable_eq α] [comm_semigroup α] :
comm_semigroup (finset α)

finset α is a comm_semigroup under pointwise operations if α is.

Equations
source
theorem finset.inter_mul_union_subset {α : Type u_2} [decidable_eq α] [comm_semigroup α] {s t : finset α} :
s ∩ t * (s ∪ t) ⊆ s * t
source
theorem finset.inter_add_union_subset {α : Type u_2} [decidable_eq α] [add_comm_semigroup α] {s t : finset α} :
s ∩ t + (s ∪ t) ⊆ s + t
source
theorem finset.union_add_inter_subset {α : Type u_2} [decidable_eq α] [add_comm_semigroup α] {s t : finset α} :
s ∪ t + s ∩ t ⊆ s + t
source
theorem finset.union_mul_inter_subset {α : Type u_2} [decidable_eq α] [comm_semigroup α] {s t : finset α} :
(s ∪ t) * (s ∩ t) ⊆ s * t
source
@[protected]
def finset.add_zero_class {α : Type u_2} [decidable_eq α] [add_zero_class α] :
add_zero_class (finset α)

finset α is an add_zero_class under pointwise operations if α is.

Equations
source
@[protected]
def finset.mul_one_class {α : Type u_2} [decidable_eq α] [mul_one_class α] :
mul_one_class (finset α)

finset α is a mul_one_class under pointwise operations if α is.

Equations
source
theorem finset.subset_mul_left {α : Type u_2} [decidable_eq α] [mul_one_class α] (s : finset α) {t : finset α} (ht : 1 ∈ t) :
s ⊆ s * t
source
theorem finset.subset_add_left {α : Type u_2} [decidable_eq α] [add_zero_class α] (s : finset α) {t : finset α} (ht : 0 ∈ t) :
s ⊆ s + t
source
theorem finset.subset_mul_right {α : Type u_2} [decidable_eq α] [mul_one_class α] {s : finset α} (t : finset α) (hs : 1 ∈ s) :
t ⊆ s * t
source
theorem finset.subset_add_right {α : Type u_2} [decidable_eq α] [add_zero_class α] {s : finset α} (t : finset α) (hs : 0 ∈ s) :
t ⊆ s + t
source
def finset.singleton_add_monoid_hom {α : Type u_2} [decidable_eq α] [add_zero_class α] :
α →+ finset α

The singleton operation as an add_monoid_hom.

Equations
source
def finset.singleton_monoid_hom {α : Type u_2} [decidable_eq α] [mul_one_class α] :
α →* finset α

The singleton operation as a monoid_hom.

Equations
source
@[simp]
theorem finset.coe_singleton_add_monoid_hom {α : Type u_2} [decidable_eq α] [add_zero_class α] :
⇑finset.singleton_add_monoid_hom = has_singleton.singleton
source
@[simp]
theorem finset.coe_singleton_monoid_hom {α : Type u_2} [decidable_eq α] [mul_one_class α] :
⇑finset.singleton_monoid_hom = has_singleton.singleton
source
@[simp]
theorem finset.singleton_add_monoid_hom_apply {α : Type u_2} [decidable_eq α] [add_zero_class α] (a : α) :
⇑finset.singleton_add_monoid_hom a = {a}
source
@[simp]
theorem finset.singleton_monoid_hom_apply {α : Type u_2} [decidable_eq α] [mul_one_class α] (a : α) :
⇑finset.singleton_monoid_hom a = {a}
source
def finset.coe_monoid_hom {α : Type u_2} [decidable_eq α] [mul_one_class α] :
finset α →* set α

The coercion from finset to set as a monoid_hom.

Equations
source
def finset.coe_add_monoid_hom {α : Type u_2} [decidable_eq α] [add_zero_class α] :
finset α →+ set α

The coercion from finset to set as an add_monoid_hom.

Equations
source
@[simp]
theorem finset.coe_coe_add_monoid_hom {α : Type u_2} [decidable_eq α] [add_zero_class α] :
⇑finset.coe_add_monoid_hom = coe
source
@[simp]
theorem finset.coe_coe_monoid_hom {α : Type u_2} [decidable_eq α] [mul_one_class α] :
⇑finset.coe_monoid_hom = coe
source
@[simp]
theorem finset.coe_add_monoid_hom_apply {α : Type u_2} [decidable_eq α] [add_zero_class α] (s : finset α) :
⇑finset.coe_add_monoid_hom s = ↑s
source
@[simp]
theorem finset.coe_monoid_hom_apply {α : Type u_2} [decidable_eq α] [mul_one_class α] (s : finset α) :
⇑finset.coe_monoid_hom s = ↑s
source
def finset.image_add_monoid_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [add_zero_class α] [add_zero_class β] [add_monoid_hom_class F α β] (f : F) :
finset α →+ finset β

Lift an add_monoid_hom to finset via image

Equations
source
@[simp]
theorem finset.image_monoid_hom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] (f : F) (ᾰ : finset α) :
⇑(finset.image_monoid_hom f) ᾰ = (finset.image_mul_hom f).to_fun ᾰ
source
def finset.image_monoid_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] (f : F) :
finset α →* finset β

Lift a monoid_hom to finset via image.

Equations
source
@[simp]
theorem finset.image_add_monoid_hom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [add_zero_class α] [add_zero_class β] [add_monoid_hom_class F α β] (f : F) (ᾰ : finset α) :
⇑(finset.image_add_monoid_hom f) ᾰ = (finset.image_add_hom f).to_fun ᾰ
source
@[simp, norm_cast]
theorem finset.coe_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] (s : finset α) (n : ℕ) :
↑(n • s) = n • ↑s
source
@[simp, norm_cast]
theorem finset.coe_pow {α : Type u_2} [decidable_eq α] [monoid α] (s : finset α) (n : ℕ) :
↑(s ^ n) = ↑s ^ n
source
@[protected]
def finset.monoid {α : Type u_2} [decidable_eq α] [monoid α] :
monoid (finset α)

finset α is a monoid under pointwise operations if α is.

Equations
source
@[protected]
def finset.add_monoid {α : Type u_2} [decidable_eq α] [add_monoid α] :
add_monoid (finset α)

finset α is an add_monoid under pointwise operations if α is.

Equations
source
theorem finset.nsmul_mem_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {a : α} (ha : a ∈ s) (n : ℕ) :
n • a ∈ n • s
source
theorem finset.pow_mem_pow {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {a : α} (ha : a ∈ s) (n : ℕ) :
a ^ n ∈ s ^ n
source
theorem finset.nsmul_subset_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {s t : finset α} (hst : s ⊆ t) (n : ℕ) :
n • s ⊆ n • t
source
theorem finset.pow_subset_pow {α : Type u_2} [decidable_eq α] [monoid α] {s t : finset α} (hst : s ⊆ t) (n : ℕ) :
s ^ n ⊆ t ^ n
source
theorem finset.pow_subset_pow_of_one_mem {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {m n : ℕ} (hs : 1 ∈ s) :
m ≤ n → s ^ m ⊆ s ^ n
source
theorem finset.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {m n : ℕ} (hs : 0 ∈ s) :
m ≤ n → m • s ⊆ n • s
source
@[simp, norm_cast]
theorem finset.coe_list_prod {α : Type u_2} [decidable_eq α] [monoid α] (s : list (finset α)) :
↑(s.prod) = (list.map coe s).prod
source
@[simp, norm_cast]
theorem finset.coe_list_sum {α : Type u_2} [decidable_eq α] [add_monoid α] (s : list (finset α)) :
↑(s.sum) = (list.map coe s).sum
source
theorem finset.mem_sum_list_of_fn {α : Type u_2} [decidable_eq α] [add_monoid α] {n : ℕ} {a : α} {s : fin n → finset α} :
a ∈ (list.of_fn s).sum ↔ ∃ (f : Π (i : fin n), ↥(s i)), (list.of_fn (λ (i : fin n), ↑(f i))).sum = a
source
theorem finset.mem_prod_list_of_fn {α : Type u_2} [decidable_eq α] [monoid α] {n : ℕ} {a : α} {s : fin n → finset α} :
a ∈ (list.of_fn s).prod ↔ ∃ (f : Π (i : fin n), ↥(s i)), (list.of_fn (λ (i : fin n), ↑(f i))).prod = a
source
theorem finset.mem_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {a : α} {n : ℕ} :
a ∈ n • s ↔ ∃ (f : fin n → ↥s), (list.of_fn (λ (i : fin n), ↑(f i))).sum = a
source
theorem finset.mem_pow {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {a : α} {n : ℕ} :
a ∈ s ^ n ↔ ∃ (f : fin n → ↥s), (list.of_fn (λ (i : fin n), ↑(f i))).prod = a
source
@[simp]
theorem finset.empty_pow {α : Type u_2} [decidable_eq α] [monoid α] {n : ℕ} (hn : n ≠ 0) :
∅ ^ n = ∅
source
@[simp]
theorem finset.empty_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {n : ℕ} (hn : n ≠ 0) :
n • ∅ = ∅
source
theorem finset.mul_univ_of_one_mem {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} [fintype α] (hs : 1 ∈ s) :
s * finset.univ = finset.univ
source
theorem finset.add_univ_of_zero_mem {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} [fintype α] (hs : 0 ∈ s) :
s + finset.univ = finset.univ
source
theorem finset.univ_mul_of_one_mem {α : Type u_2} [decidable_eq α] [monoid α] {t : finset α} [fintype α] (ht : 1 ∈ t) :
finset.univ * t = finset.univ
source
theorem finset.univ_add_of_zero_mem {α : Type u_2} [decidable_eq α] [add_monoid α] {t : finset α} [fintype α] (ht : 0 ∈ t) :
finset.univ + t = finset.univ
source
@[simp]
theorem finset.univ_mul_univ {α : Type u_2} [decidable_eq α] [monoid α] [fintype α] :
finset.univ * finset.univ = finset.univ
source
@[simp]
theorem finset.univ_add_univ {α : Type u_2} [decidable_eq α] [add_monoid α] [fintype α] :
finset.univ + finset.univ = finset.univ
source
@[simp]
theorem finset.nsmul_univ {α : Type u_2} [decidable_eq α] [add_monoid α] {n : ℕ} [fintype α] (hn : n ≠ 0) :
n • finset.univ = finset.univ
source
@[simp]
theorem finset.univ_pow {α : Type u_2} [decidable_eq α] [monoid α] {n : ℕ} [fintype α] (hn : n ≠ 0) :
finset.univ ^ n = finset.univ
source
@[protected]
theorem is_add_unit.finset {α : Type u_2} [decidable_eq α] [add_monoid α] {a : α} :
is_add_unit a → is_add_unit {a}
source
@[protected]
theorem is_unit.finset {α : Type u_2} [decidable_eq α] [monoid α] {a : α} :
is_unit a → is_unit {a}
source
@[protected]
def finset.comm_monoid {α : Type u_2} [decidable_eq α] [comm_monoid α] :
comm_monoid (finset α)

finset α is a comm_monoid under pointwise operations if α is.

Equations
source
@[protected]
def finset.add_comm_monoid {α : Type u_2} [decidable_eq α] [add_comm_monoid α] :
add_comm_monoid (finset α)

finset α is an add_comm_monoid under pointwise operations if α is.

Equations
source
@[simp, norm_cast]
theorem finset.coe_prod {α : Type u_2} [decidable_eq α] [comm_monoid α] {ι : Type u_1} (s : finset ι) (f : ι → finset α) :
↑(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), ↑(f i))
source
@[simp, norm_cast]
theorem finset.coe_sum {α : Type u_2} [decidable_eq α] [add_comm_monoid α] {ι : Type u_1} (s : finset ι) (f : ι → finset α) :
↑(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ↑(f i))
source
@[simp]
theorem finset.coe_zsmul {α : Type u_2} [decidable_eq α] [subtraction_monoid α] (s : finset α) (n : ℤ) :
↑(n • s) = n • ↑s
source
@[simp]
theorem finset.coe_zpow {α : Type u_2} [decidable_eq α] [division_monoid α] (s : finset α) (n : ℤ) :
↑(s ^ n) = ↑s ^ n
source
@[protected]
theorem finset.mul_eq_one_iff {α : Type u_2} [decidable_eq α] [division_monoid α] {s t : finset α} :
s * t = 1 ↔ ∃ (a b : α), s = {a} ∧ t = {b} ∧ a * b = 1
source
@[protected]
theorem finset.add_eq_zero_iff {α : Type u_2} [decidable_eq α] [subtraction_monoid α] {s t : finset α} :
s + t = 0 ↔ ∃ (a b : α), s = {a} ∧ t = {b} ∧ a + b = 0
source
@[protected]
def finset.division_monoid {α : Type u_2} [decidable_eq α] [division_monoid α] :
division_monoid (finset α)

finset α is a division monoid under pointwise operations if α is.

Equations
source
@[protected]
def finset.subtraction_monoid {α : Type u_2} [decidable_eq α] [subtraction_monoid α] :
subtraction_monoid (finset α)

finset α is a subtraction monoid under pointwise operations if α is.

Equations
source
@[simp]
theorem finset.is_add_unit_iff {α : Type u_2} [decidable_eq α] [subtraction_monoid α] {s : finset α} :
is_add_unit s ↔ ∃ (a : α), s = {a} ∧ is_add_unit a
source
@[simp]
theorem finset.is_unit_iff {α : Type u_2} [decidable_eq α] [division_monoid α] {s : finset α} :
is_unit s ↔ ∃ (a : α), s = {a} ∧ is_unit a
source
@[simp]
theorem finset.is_add_unit_coe {α : Type u_2} [decidable_eq α] [subtraction_monoid α] {s : finset α} :
is_add_unit ↑s ↔ is_add_unit s
source
@[simp]
theorem finset.is_unit_coe {α : Type u_2} [decidable_eq α] [division_monoid α] {s : finset α} :
is_unit ↑s ↔ is_unit s
source
@[protected]
def finset.subtraction_comm_monoid {α : Type u_2} [decidable_eq α] [subtraction_comm_monoid α] :
subtraction_comm_monoid (finset α)

finset α is a commutative subtraction monoid under pointwise operations if α is.

Equations
source
@[protected]
def finset.division_comm_monoid {α : Type u_2} [decidable_eq α] [division_comm_monoid α] :
division_comm_monoid (finset α)

finset α is a commutative division monoid under pointwise operations if α is.

Equations
source
@[protected]
def finset.has_distrib_neg {α : Type u_2} [decidable_eq α] [has_mul α] [has_distrib_neg α] :
has_distrib_neg (finset α)

finset α has distributive negation if α has.

Equations

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_2} [decidable_eq α] [distrib α] (s t u : finset α) :
s * (t + u) ⊆ s * t + s * u
source
theorem finset.add_mul_subset {α : Type u_2} [decidable_eq α] [distrib α] (s t u : finset α) :
(s + t) * u ⊆ s * u + t * u

Note that finset is not a mul_zero_class because 0 * ∅ ≠ 0.

source
theorem finset.mul_zero_subset {α : Type u_2} [decidable_eq α] [mul_zero_class α] (s : finset α) :
s * 0 ⊆ 0
source
theorem finset.zero_mul_subset {α : Type u_2} [decidable_eq α] [mul_zero_class α] (s : finset α) :
0 * s ⊆ 0
source
theorem finset.nonempty.mul_zero {α : Type u_2} [decidable_eq α] [mul_zero_class α] {s : finset α} (hs : s.nonempty) :
s * 0 = 0
source
theorem finset.nonempty.zero_mul {α : Type u_2} [decidable_eq α] [mul_zero_class α] {s : finset α} (hs : s.nonempty) :
0 * s = 0

Note that finset is not a group because s / s ≠ 1 in general.

source
@[simp]
theorem finset.one_mem_div_iff {α : Type u_2} [decidable_eq α] [group α] {s t : finset α} :
1 ∈ s / t ↔ ¬disjoint s t
source
@[simp]
theorem finset.zero_mem_sub_iff {α : Type u_2} [decidable_eq α] [add_group α] {s t : finset α} :
0 ∈ s - t ↔ ¬disjoint s t
source
theorem finset.not_one_mem_div_iff {α : Type u_2} [decidable_eq α] [group α] {s t : finset α} :
1 ∉ s / t ↔ disjoint s t
source
theorem finset.not_zero_mem_sub_iff {α : Type u_2} [decidable_eq α] [add_group α] {s t : finset α} :
0 ∉ s - t ↔ disjoint s t
source
theorem finset.nonempty.zero_mem_sub {α : Type u_2} [decidable_eq α] [add_group α] {s : finset α} (h : s.nonempty) :
0 ∈ s - s
source
theorem finset.nonempty.one_mem_div {α : Type u_2} [decidable_eq α] [group α] {s : finset α} (h : s.nonempty) :
1 ∈ s / s
source
theorem finset.is_add_unit_singleton {α : Type u_2} [decidable_eq α] [add_group α] (a : α) :
is_add_unit {a}
source
theorem finset.is_unit_singleton {α : Type u_2} [decidable_eq α] [group α] (a : α) :
is_unit {a}
source
@[simp]
theorem finset.is_unit_iff_singleton {α : Type u_2} [decidable_eq α] [group α] {s : finset α} :
is_unit s ↔ ∃ (a : α), s = {a}
source
@[simp]
theorem finset.image_mul_left {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {a : α} :
finset.image (λ (b : α), a * b) t = t.preimage (λ (b : α), a⁻¹ * b) _
source
@[simp]
theorem finset.image_add_left {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {a : α} :
finset.image (λ (b : α), a + b) t = t.preimage (λ (b : α), -a + b) _
source
@[simp]
theorem finset.image_mul_right {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x * b) t = t.preimage (λ (_x : α), _x * b⁻¹) _
source
@[simp]
theorem finset.image_add_right {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x + b) t = t.preimage (λ (_x : α), _x + -b) _
source
theorem finset.image_add_left' {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {a : α} :
finset.image (λ (b : α), -a + b) t = t.preimage (λ (b : α), a + b) _
source
theorem finset.image_mul_left' {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {a : α} :
finset.image (λ (b : α), a⁻¹ * b) t = t.preimage (λ (b : α), a * b) _
source
theorem finset.image_add_right' {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x + -b) t = t.preimage (λ (_x : α), _x + b) _
source
theorem finset.image_mul_right' {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x * b⁻¹) t = t.preimage (λ (_x : α), _x * b) _
source
theorem finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [group α] [division_monoid β] [monoid_hom_class F α β] (f : F) {s t : finset α} :
finset.image ⇑f (s / t) = finset.image ⇑f s / finset.image ⇑f t
source
theorem finset.div_zero_subset {α : Type u_2} [decidable_eq α] [group_with_zero α] (s : finset α) :
s / 0 ⊆ 0
source
theorem finset.zero_div_subset {α : Type u_2} [decidable_eq α] [group_with_zero α] (s : finset α) :
0 / s ⊆ 0
source
theorem finset.nonempty.div_zero {α : Type u_2} [decidable_eq α] [group_with_zero α] {s : finset α} (hs : s.nonempty) :
s / 0 = 0
source
theorem finset.nonempty.zero_div {α : Type u_2} [decidable_eq α] [group_with_zero α] {s : finset α} (hs : s.nonempty) :
0 / s = 0
source
@[simp]
theorem finset.preimage_mul_left_singleton {α : Type u_2} [group α] {a b : α} :
{b}.preimage (has_mul.mul a) _ = {a⁻¹ * b}
source
@[simp]
theorem finset.preimage_add_left_singleton {α : Type u_2} [add_group α] {a b : α} :
{b}.preimage (has_add.add a) _ = {-a + b}
source
@[simp]
theorem finset.preimage_mul_right_singleton {α : Type u_2} [group α] {a b : α} :
{b}.preimage (λ (_x : α), _x * a) _ = {b * a⁻¹}
source
@[simp]
theorem finset.preimage_add_right_singleton {α : Type u_2} [add_group α] {a b : α} :
{b}.preimage (λ (_x : α), _x + a) _ = {b + -a}
source
@[simp]
theorem finset.preimage_mul_left_one {α : Type u_2} [group α] {a : α} :
1.preimage (has_mul.mul a) _ = {a⁻¹}
source
@[simp]
theorem finset.preimage_add_left_zero {α : Type u_2} [add_group α] {a : α} :
0.preimage (has_add.add a) _ = {-a}
source
@[simp]
theorem finset.preimage_add_right_zero {α : Type u_2} [add_group α] {b : α} :
0.preimage (λ (_x : α), _x + b) _ = {-b}
source
@[simp]
theorem finset.preimage_mul_right_one {α : Type u_2} [group α] {b : α} :
1.preimage (λ (_x : α), _x * b) _ = {b⁻¹}
source
theorem finset.preimage_add_left_zero' {α : Type u_2} [add_group α] {a : α} :
0.preimage (has_add.add (-a)) _ = {a}
source
theorem finset.preimage_mul_left_one' {α : Type u_2} [group α] {a : α} :
1.preimage (has_mul.mul a⁻¹) _ = {a}
source
theorem finset.preimage_mul_right_one' {α : Type u_2} [group α] {b : α} :
1.preimage (λ (_x : α), _x * b⁻¹) _ = {b}
source
theorem finset.preimage_add_right_zero' {α : Type u_2} [add_group α] {b : α} :
0.preimage (λ (_x : α), _x + -b) _ = {b}

Scalar addition/multiplication of finsets #

source
@[protected]
def finset.has_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] :
has_smul (finset α) (finset β)

The pointwise product of two finsets s and t: s • t = {x • y | x ∈ s, y ∈ t}.

Equations
source
@[protected]
def finset.has_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] :
has_vadd (finset α) (finset β)

The pointwise sum of two finsets s and t: s +ᵥ t = {x +ᵥ y | x ∈ s, y ∈ t}.

Equations
source
theorem finset.smul_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
s • t = finset.image (λ (p : α × β), p.fst • p.snd) (s ×ˢ t)
source
theorem finset.vadd_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
s +ᵥ t = finset.image (λ (p : α × β), p.fst +ᵥ p.snd) (s ×ˢ t)
source
theorem finset.image_smul_product {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
finset.image (λ (x : α × β), x.fst • x.snd) (s ×ˢ t) = s • t
source
theorem finset.image_vadd_product {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
finset.image (λ (x : α × β), x.fst +ᵥ x.snd) (s ×ˢ t) = s +ᵥ t
source
theorem finset.mem_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} {x : β} :
x ∈ s • t ↔ ∃ (y : α) (z : β), y ∈ s ∧ z ∈ t ∧ y • z = x
source
theorem finset.mem_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} {x : β} :
x ∈ s +ᵥ t ↔ ∃ (y : α) (z : β), y ∈ s ∧ z ∈ t ∧ y +ᵥ z = x
source
@[simp, norm_cast]
theorem finset.coe_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (s : finset α) (t : finset β) :
↑(s +ᵥ t) = ↑s +ᵥ ↑t
source
@[simp, norm_cast]
theorem finset.coe_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (s : finset α) (t : finset β) :
↑(s • t) = ↑s • ↑t
source
theorem finset.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} {a : α} {b : β} :
a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t
source
theorem finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} {a : α} {b : β} :
a ∈ s → b ∈ t → a • b ∈ s • t
source
theorem finset.vadd_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).card ≤ s.card • t.card
source
theorem finset.smul_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s • t).card ≤ s.card • t.card
source
@[simp]
theorem finset.empty_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (t : finset β) :
∅ • t = ∅
source
@[simp]
theorem finset.empty_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (t : finset β) :
∅ +ᵥ t = ∅
source
@[simp]
theorem finset.vadd_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (s : finset α) :
s +ᵥ ∅ = ∅
source
@[simp]
theorem finset.smul_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (s : finset α) :
s • ∅ = ∅
source
@[simp]
theorem finset.vadd_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.smul_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
s • t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s • t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[simp]
theorem finset.vadd_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem finset.nonempty.smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
s.nonempty → t.nonempty → (s • t).nonempty
source
theorem finset.nonempty.vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
s.nonempty → t.nonempty → (s +ᵥ t).nonempty
source
theorem finset.nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty → s.nonempty
source
theorem finset.nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s • t).nonempty → s.nonempty
source
theorem finset.nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty → t.nonempty
source
theorem finset.nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s • t).nonempty → t.nonempty
source
theorem finset.vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} (b : β) :
s +ᵥ {b} = finset.image (λ (_x : α), _x +ᵥ b) s
source
theorem finset.smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} (b : β) :
s • {b} = finset.image (λ (_x : α), _x • b) s
source
theorem finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) (b : β) :
{a} +ᵥ {b} = {a +ᵥ b}
source
theorem finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) (b : β) :
{a} • {b} = {a • b}
source
theorem finset.smul_subset_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂
source
theorem finset.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂
source
theorem finset.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t₁ t₂ : finset β} :
t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂
source
theorem finset.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t₁ t₂ : finset β} :
t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
source
theorem finset.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t : finset β} :
s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t
source
theorem finset.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t : finset β} :
s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
source
theorem finset.smul_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t u : finset β} :
s • t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → a • b ∈ u
source
theorem finset.vadd_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t u : finset β} :
s +ᵥ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → a +ᵥ b ∈ u
source
theorem finset.union_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
(s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t
source
theorem finset.union_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
s₁ ∪ s₂ +ᵥ t = s₁ +ᵥ t ∪ (s₂ +ᵥ t)
source
theorem finset.vadd_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t₁ t₂ : finset β} :
s +ᵥ (t₁ ∪ t₂) = s +ᵥ t₁ ∪ (s +ᵥ t₂)
source
theorem finset.smul_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t₁ t₂ : finset β} :
s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂
source
theorem finset.inter_vadd_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)
source
theorem finset.inter_smul_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
(s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t
source
theorem finset.smul_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t₁ t₂ : finset β} :
s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂
source
theorem finset.vadd_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t₁ t₂ : finset β} :
s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)
source
theorem finset.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} [decidable_eq α] :
s₁ ∩ s₂ +ᵥ (t₁ ∪ t₂) ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)
source
theorem finset.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} [decidable_eq α] :
(s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
source
theorem finset.union_smul_inter_subset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} [decidable_eq α] :
(s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
source
theorem finset.union_vadd_inter_subset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} [decidable_eq α] :
s₁ ∪ s₂ +ᵥ t₁ ∩ t₂ ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)
source
theorem finset.subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {u : finset β} {s : set α} {t : set β} :
↑u ⊆ s +ᵥ t → (∃ (s' : finset α) (t' : finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' +ᵥ t')

If a finset u is contained in the scalar sum of two sets s +ᵥ t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' +ᵥ t'.

source
theorem finset.subset_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {u : finset β} {s : set α} {t : set β} :
↑u ⊆ s • t → (∃ (s' : finset α) (t' : finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t')

If a finset u is contained in the scalar product of two sets s • t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' • t'.

Scalar subtraction of finsets #

source
@[protected]
def finset.has_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] :
has_vsub (finset α) (finset β)

The pointwise product of two finsets s and t: s -ᵥ t = {x -ᵥ y | x ∈ s, y ∈ t}.

Equations
source
theorem finset.vsub_def {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
s -ᵥ t = finset.image₂ has_vsub.vsub s t
source
@[simp]
theorem finset.image_vsub_product {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
finset.image₂ has_vsub.vsub s t = s -ᵥ t
source
theorem finset.mem_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} {a : α} :
a ∈ s -ᵥ t ↔ ∃ (b c : β), b ∈ s ∧ c ∈ t ∧ b -ᵥ c = a
source
@[simp, norm_cast]
theorem finset.coe_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (s t : finset β) :
↑(s -ᵥ t) = ↑s -ᵥ ↑t
source
theorem finset.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} {b c : β} :
b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t
source
theorem finset.vsub_card_le {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).card ≤ s.card * t.card
source
@[simp]
theorem finset.empty_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (t : finset β) :
∅ -ᵥ t = ∅
source
@[simp]
theorem finset.vsub_empty {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (s : finset β) :
s -ᵥ ∅ = ∅
source
@[simp]
theorem finset.vsub_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.vsub_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem finset.nonempty.vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
s.nonempty → t.nonempty → (s -ᵥ t).nonempty
source
theorem finset.nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).nonempty → s.nonempty
source
theorem finset.nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).nonempty → t.nonempty
source
@[simp]
theorem finset.vsub_singleton {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s : finset β} (b : β) :
s -ᵥ {b} = finset.image (λ (_x : β), _x -ᵥ b) s
source
theorem finset.singleton_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {t : finset β} (a : β) :
{a} -ᵥ t = finset.image (has_vsub.vsub a) t
source
@[simp]
theorem finset.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (a b : β) :
{a} -ᵥ {b} = {a -ᵥ b}
source
theorem finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t₁ t₂ : finset β} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
source
theorem finset.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t₁ t₂ : finset β} :
t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
source
theorem finset.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t : finset β} :
s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
source
theorem finset.vsub_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} {u : finset α} :
s -ᵥ t ⊆ u ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ t → x -ᵥ y ∈ u
source
theorem finset.union_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t : finset β} [decidable_eq β] :
s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
source
theorem finset.vsub_union {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t₁ t₂ : finset β} [decidable_eq β] :
s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
source
theorem finset.inter_vsub_subset {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t : finset β} [decidable_eq β] :
s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)
source
theorem finset.vsub_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t₁ t₂ : finset β} [decidable_eq β] :
s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)
source
theorem finset.subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {u : finset α} {s t : set β} :
↑u ⊆ s -ᵥ t → (∃ (s' t' : finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' -ᵥ t')

If a finset u is contained in the pointwise subtraction of two sets s -ᵥ t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' -ᵥ t'.

Translation/scaling of finsets #

source
@[protected]
def finset.has_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] :
has_vadd α (finset β)

The translation of a finset s by a vector a: a +ᵥ s = {a +ᵥ x | x ∈ s}.

Equations
source
@[protected]
def finset.has_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] :
has_smul α (finset β)

The scaling of a finset s by a scalar a: a • s = {a • x | x ∈ s}.

Equations
source
theorem finset.smul_finset_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
a • s = finset.image (has_smul.smul a) s
source
theorem finset.vadd_finset_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
a +ᵥ s = finset.image (has_vadd.vadd a) s
source
theorem finset.image_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
finset.image (λ (x : β), a +ᵥ x) s = a +ᵥ s
source
theorem finset.image_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
finset.image (λ (x : β), a • x) s = a • s
source
theorem finset.mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} {x : β} :
x ∈ a • s ↔ ∃ (y : β), y ∈ s ∧ a • y = x
source
theorem finset.mem_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} {x : β} :
x ∈ a +ᵥ s ↔ ∃ (y : β), y ∈ s ∧ a +ᵥ y = x
source
@[simp, norm_cast]
theorem finset.coe_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) (s : finset β) :
↑(a • s) = a • ↑s
source
@[simp, norm_cast]
theorem finset.coe_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) (s : finset β) :
↑(a +ᵥ s) = a +ᵥ ↑s
source
theorem finset.smul_mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} {b : β} :
b ∈ s → a • b ∈ a • s
source
theorem finset.vadd_mem_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} {b : β} :
b ∈ s → a +ᵥ b ∈ a +ᵥ s
source
theorem finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
(a +ᵥ s).card ≤ s.card
source
theorem finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
(a • s).card ≤ s.card
source
@[simp]
theorem finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) :
a +ᵥ ∅ = ∅
source
@[simp]
theorem finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) :
a • ∅ = ∅
source
@[simp]
theorem finset.vadd_finset_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
a +ᵥ s = ∅ ↔ s = ∅
source
@[simp]
theorem finset.smul_finset_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
a • s = ∅ ↔ s = ∅
source
@[simp]
theorem finset.vadd_finset_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
(a +ᵥ s).nonempty ↔ s.nonempty
source
@[simp]
theorem finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
(a • s).nonempty ↔ s.nonempty
source
theorem finset.nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} (hs : s.nonempty) :
(a +ᵥ s).nonempty
source
theorem finset.nonempty.smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} (hs : s.nonempty) :
(a • s).nonempty
source
@[simp]
theorem finset.singleton_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {t : finset β} (a : α) :
{a} • t = a • t
source
@[simp]
theorem finset.singleton_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {t : finset β} (a : α) :
{a} +ᵥ t = a +ᵥ t
source
theorem finset.vadd_finset_subset_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s t : finset β} {a : α} :
s ⊆ t → a +ᵥ s ⊆ a +ᵥ t
source
theorem finset.smul_finset_subset_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s t : finset β} {a : α} :
s ⊆ t → a • s ⊆ a • t
source
@[simp]
theorem finset.smul_finset_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {a : α} (b : β) :
a • {b} = {a • b}
source
@[simp]
theorem finset.vadd_finset_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {a : α} (b : β) :
a +ᵥ {b} = {a +ᵥ b}
source
theorem finset.vadd_finset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset β} {a : α} :
a +ᵥ (s₁ ∪ s₂) = a +ᵥ s₁ ∪ (a +ᵥ s₂)
source
theorem finset.smul_finset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset β} {a : α} :
a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂
source
theorem finset.smul_finset_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset β} {a : α} :
a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ a • s₂
source
theorem finset.vadd_finset_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset β} {a : α} :
a +ᵥ s₁ ∩ s₂ ⊆ (a +ᵥ s₁) ∩ (a +ᵥ s₂)
source
theorem finset.vadd_finset_subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {t : finset β} {a : α} {s : finset α} :
a ∈ s → a +ᵥ t ⊆ s +ᵥ t
source
theorem finset.smul_finset_subset_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {t : finset β} {a : α} {s : finset α} :
a ∈ s → a • t ⊆ s • t
source
@[simp]
theorem finset.bUnion_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (s : finset α) (t : finset β) :
s.bUnion (λ (_x : α), _x +ᵥ t) = s +ᵥ t
source
@[simp]
theorem finset.bUnion_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (s : finset α) (t : finset β) :
s.bUnion (λ (_x : α), _x • t) = s • t
source
@[protected, instance]
def finset.vadd_comm_class_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class α β (finset γ)
source
@[protected, instance]
def finset.smul_comm_class_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class α β (finset γ)
source
@[protected, instance]
def finset.vadd_comm_class_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class α (finset β) (finset γ)
source
@[protected, instance]
def finset.smul_comm_class_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class α (finset β) (finset γ)
source
@[protected, instance]
def finset.vadd_comm_class_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class (finset α) β (finset γ)
source
@[protected, instance]
def finset.smul_comm_class_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class (finset α) β (finset γ)
source
@[protected, instance]
def finset.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class (finset α) (finset β) (finset γ)
source
@[protected, instance]
def finset.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class (finset α) (finset β) (finset γ)
source
@[protected, instance]
def finset.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower α β (finset γ)
source
@[protected, instance]
def finset.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class α β (finset γ)
source
@[protected, instance]
def finset.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower α (finset β) (finset γ)
source
@[protected, instance]
def finset.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class α (finset β) (finset γ)
source
@[protected, instance]
def finset.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class (finset α) (finset β) (finset γ)
source
@[protected, instance]
def finset.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower (finset α) (finset β) (finset γ)
source
@[protected, instance]
def finset.is_central_scalar {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] [has_smul αᵐᵒᵖ β] [is_central_scalar α β] :
is_central_scalar α (finset β)
source
@[protected, instance]
def finset.is_central_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] [has_vadd αᵃᵒᵖ β] [is_central_vadd α β] :
is_central_vadd α (finset β)
source
@[protected]
def finset.mul_action {α : Type u_2} {β : Type u_3} [decidable_eq β] [decidable_eq α] [monoid α] [mul_action α β] :
mul_action (finset α) (finset β)

A multiplicative action of a monoid α on a type β gives a multiplicative action of finset α on finset β.

Equations
source
@[protected]
def finset.add_action {α : Type u_2} {β : Type u_3} [decidable_eq β] [decidable_eq α] [add_monoid α] [add_action α β] :
add_action (finset α) (finset β)

An additive action of an additive monoid α on a type β gives an additive action of finset α on finset β

Equations
source
@[protected]
def finset.add_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_monoid α] [add_action α β] :
add_action α (finset β)

An additive action of an additive monoid on a type β gives an additive action on finset β.

Equations
source
@[protected]
def finset.mul_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [monoid α] [mul_action α β] :
mul_action α (finset β)

A multiplicative action of a monoid on a type β gives a multiplicative action on finset β.

Equations
source
@[protected]
def finset.distrib_mul_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [monoid α] [add_monoid β] [distrib_mul_action α β] :
distrib_mul_action α (finset β)

A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on finset β.

Equations
source
@[protected]
def finset.mul_distrib_mul_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [monoid α] [monoid β] [mul_distrib_mul_action α β] :
mul_distrib_mul_action α (finset β)

A multiplicative action of a monoid on a monoid β gives a multiplicative action on set β.

Equations
source
@[protected, instance]
def finset.no_zero_divisors {α : Type u_2} [decidable_eq α] [has_zero α] [has_mul α] [no_zero_divisors α] :
no_zero_divisors (finset α)
source
@[protected, instance]
def finset.no_zero_smul_divisors {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :
no_zero_smul_divisors (finset α) (finset β)
source
@[protected, instance]
def finset.no_zero_smul_divisors_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :
no_zero_smul_divisors α (finset β)
source
theorem finset.op_vadd_finset_vadd_eq_vadd_vadd_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq β] [decidable_eq γ] [has_vadd αᵃᵒᵖ β] [has_vadd β γ] [has_vadd α γ] (a : α) (s : finset β) (t : finset γ) (h : ∀ (a : α) (b : β) (c : γ), add_opposite.op a +ᵥ b +ᵥ c = b +ᵥ (a +ᵥ c)) :
add_opposite.op a +ᵥ s +ᵥ t = s +ᵥ (a +ᵥ t)
source
theorem finset.op_smul_finset_smul_eq_smul_smul_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq β] [decidable_eq γ] [has_smul αᵐᵒᵖ β] [has_smul β γ] [has_smul α γ] (a : α) (s : finset β) (t : finset γ) (h : ∀ (a : α) (b : β) (c : γ), (mul_opposite.op a • b) • c = b • a • c) :
(mul_opposite.op a • s) • t = s • a • t
source
theorem finset.op_vadd_finset_subset_add {α : Type u_2} [has_add α] [decidable_eq α] {s t : finset α} {a : α} :
a ∈ t → add_opposite.op a +ᵥ s ⊆ s + t
source
theorem finset.op_smul_finset_subset_mul {α : Type u_2} [has_mul α] [decidable_eq α] {s t : finset α} {a : α} :
a ∈ t → mul_opposite.op a • s ⊆ s * t
source
@[simp]
theorem finset.bUnion_op_vadd_finset {α : Type u_2} [has_add α] [decidable_eq α] (s t : finset α) :
t.bUnion (λ (a : α), add_opposite.op a +ᵥ s) = s + t
source
@[simp]
theorem finset.bUnion_op_smul_finset {α : Type u_2} [has_mul α] [decidable_eq α] (s t : finset α) :
t.bUnion (λ (a : α), mul_opposite.op a • s) = s * t
source
theorem finset.add_subset_iff_left {α : Type u_2} [has_add α] [decidable_eq α] {s t u : finset α} :
s + t ⊆ u ↔ ∀ (a : α), a ∈ s → a +ᵥ t ⊆ u
source
theorem finset.mul_subset_iff_left {α : Type u_2} [has_mul α] [decidable_eq α] {s t u : finset α} :
s * t ⊆ u ↔ ∀ (a : α), a ∈ s → a • t ⊆ u
source
theorem finset.mul_subset_iff_right {α : Type u_2} [has_mul α] [decidable_eq α] {s t u : finset α} :
s * t ⊆ u ↔ ∀ (b : α), b ∈ t → mul_opposite.op b • s ⊆ u
source
theorem finset.add_subset_iff_right {α : Type u_2} [has_add α] [decidable_eq α] {s t u : finset α} :
s + t ⊆ u ↔ ∀ (b : α), b ∈ t → add_opposite.op b +ᵥ s ⊆ u
source
theorem finset.op_smul_finset_mul_eq_mul_smul_finset {α : Type u_2} [semigroup α] [decidable_eq α] (a : α) (s t : finset α) :
mul_opposite.op a • s * t = s * a • t
source
theorem finset.op_vadd_finset_add_eq_add_vadd_finset {α : Type u_2} [add_semigroup α] [decidable_eq α] (a : α) (s t : finset α) :
add_opposite.op a +ᵥ s + t = s + (a +ᵥ t)
source
theorem finset.pairwise_disjoint_smul_iff {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] {s : set α} {t : finset α} :
s.pairwise_disjoint (λ (_x : α), _x • t) ↔ set.inj_on (λ (p : α × α), p.fst * p.snd) (s ×ˢ ↑t)
source
theorem finset.pairwise_disjoint_vadd_iff {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] {s : set α} {t : finset α} :
s.pairwise_disjoint (λ (_x : α), _x +ᵥ t) ↔ set.inj_on (λ (p : α × α), p.fst + p.snd) (s ×ˢ ↑t)
source
@[simp]
theorem finset.card_singleton_add {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] (t : finset α) (a : α) :
({a} + t).card = t.card
source
@[simp]
theorem finset.card_singleton_mul {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] (t : finset α) (a : α) :
({a} * t).card = t.card
source
theorem finset.singleton_mul_inter {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
{a} * (s ∩ t) = {a} * s ∩ ({a} * t)
source
theorem finset.singleton_add_inter {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
{a} + s ∩ t = ({a} + s) ∩ ({a} + t)
source
theorem finset.card_le_card_add_left {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] (t : finset α) {s : finset α} (hs : s.nonempty) :
t.card ≤ (s + t).card
source
theorem finset.card_le_card_mul_left {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] (t : finset α) {s : finset α} (hs : s.nonempty) :
t.card ≤ (s * t).card
source
@[simp]
theorem finset.card_add_singleton {α : Type u_2} [add_right_cancel_semigroup α] [decidable_eq α] (s : finset α) (a : α) :
(s + {a}).card = s.card
source
@[simp]
theorem finset.card_mul_singleton {α : Type u_2} [right_cancel_semigroup α] [decidable_eq α] (s : finset α) (a : α) :
(s * {a}).card = s.card
source
theorem finset.inter_add_singleton {α : Type u_2} [add_right_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
s ∩ t + {a} = (s + {a}) ∩ (t + {a})
source
theorem finset.inter_mul_singleton {α : Type u_2} [right_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
s ∩ t * {a} = s * {a} ∩ (t * {a})
source
theorem finset.card_le_card_add_right {α : Type u_2} [add_right_cancel_semigroup α] [decidable_eq α] (s : finset α) {t : finset α} (ht : t.nonempty) :
s.card ≤ (s + t).card
source
theorem finset.card_le_card_mul_right {α : Type u_2} [right_cancel_semigroup α] [decidable_eq α] (s : finset α) {t : finset α} (ht : t.nonempty) :
s.card ≤ (s * t).card
source
theorem finset.image_smul_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq β] [decidable_eq γ] [has_smul α β] [has_smul α γ] (f : β → γ) (a : α) (s : finset β) :
(∀ (b : β), f (a • b) = a • f b) → finset.image f (a • s) = a • finset.image f s
source
theorem finset.image_vadd_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq β] [decidable_eq γ] [has_vadd α β] [has_vadd α γ] (f : β → γ) (a : α) (s : finset β) :
(∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → finset.image f (a +ᵥ s) = a +ᵥ finset.image f s
source
theorem finset.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [monoid α] [monoid β] [monoid_hom_class F α β] (f : F) (a : α) (s : finset α) :
finset.image ⇑f (a • s) = ⇑f a • finset.image ⇑f s
source
theorem finset.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [add_monoid α] [add_monoid β] [add_monoid_hom_class F α β] (f : F) (a : α) (s : finset α) :
finset.image ⇑f (a +ᵥ s) = ⇑f a +ᵥ finset.image ⇑f s
source
@[simp]
theorem finset.vadd_mem_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s : finset β} {b : β} (a : α) :
a +ᵥ b ∈ a +ᵥ s ↔ b ∈ s
source
@[simp]
theorem finset.smul_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s : finset β} {b : β} (a : α) :
a • b ∈ a • s ↔ b ∈ s
source
theorem finset.neg_vadd_mem_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s : finset β} {a : α} {b : β} :
-a +ᵥ b ∈ s ↔ b ∈ a +ᵥ s
source
theorem finset.inv_smul_mem_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s : finset β} {a : α} {b : β} :
a⁻¹ • b ∈ s ↔ b ∈ a • s
source
theorem finset.mem_inv_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s : finset β} {a : α} {b : β} :
b ∈ a⁻¹ • s ↔ a • b ∈ s
source
theorem finset.mem_neg_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s : finset β} {a : α} {b : β} :
b ∈ -a +ᵥ s ↔ a +ᵥ b ∈ s
source
@[simp]
theorem finset.vadd_finset_subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t
source
@[simp]
theorem finset.smul_finset_subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a • s ⊆ a • t ↔ s ⊆ t
source
theorem finset.vadd_finset_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s ⊆ t ↔ s ⊆ -a +ᵥ t
source
theorem finset.smul_finset_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a • s ⊆ t ↔ s ⊆ a⁻¹ • t
source
theorem finset.subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
s ⊆ a +ᵥ t ↔ -a +ᵥ s ⊆ t
source
theorem finset.subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
s ⊆ a • t ↔ a⁻¹ • s ⊆ t
source
theorem finset.vadd_finset_inter {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
source
theorem finset.smul_finset_inter {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a • (s ∩ t) = a • s ∩ a • t
source
theorem finset.smul_finset_sdiff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a • (s \ t) = a • s \ a • t
source
theorem finset.vadd_finset_sdiff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
source
theorem finset.smul_finset_symm_diff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a • s ∆ t = (a • s) ∆ (a • t)
source
theorem finset.vadd_finset_symm_diff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s ∆ t = (a +ᵥ s) ∆ (a +ᵥ t)
source
@[simp]
theorem finset.smul_finset_univ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {a : α} [fintype β] :
a • finset.univ = finset.univ
source
@[simp]
theorem finset.vadd_finset_univ {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {a : α} [fintype β] :
a +ᵥ finset.univ = finset.univ
source
@[simp]
theorem finset.vadd_univ {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] [fintype β] {s : finset α} (hs : s.nonempty) :
s +ᵥ finset.univ = finset.univ
source
@[simp]
theorem finset.smul_univ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] [fintype β] {s : finset α} (hs : s.nonempty) :
s • finset.univ = finset.univ
source
@[simp]
theorem finset.card_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] (a : α) (s : finset β) :
(a • s).card = s.card
source
@[simp]
theorem finset.card_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] (a : α) (s : finset β) :
(a +ᵥ s).card = s.card
source
theorem finset.card_dvd_card_vadd_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {t : finset β} {s : finset α} :
((λ (_x : α), _x +ᵥ t) '' ↑s).pairwise_disjoint id → t.card ∣ (s +ᵥ t).card

If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s + t.

source
theorem finset.card_dvd_card_smul_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {t : finset β} {s : finset α} :
((λ (_x : α), _x • t) '' ↑s).pairwise_disjoint id → t.card ∣ (s • t).card

If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s * t.

source
theorem finset.card_dvd_card_mul_left {α : Type u_2} [group α] [decidable_eq α] {s t : finset α} :
((λ (b : α), finset.image (λ (a : α), a * b) s) '' ↑t).pairwise_disjoint id → s.card ∣ (s * t).card

If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then the size of s divides the size of s * t.

source
theorem finset.card_dvd_card_add_left {α : Type u_2} [add_group α] [decidable_eq α] {s t : finset α} :
((λ (b : α), finset.image (λ (a : α), a + b) s) '' ↑t).pairwise_disjoint id → s.card ∣ (s + t).card

If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then the size of s divides the size of s + t.

source
@[simp]
theorem finset.smul_mem_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s : finset β} {a : α} {b : β} (ha : a ≠ 0) :
a • b ∈ a • s ↔ b ∈ s
source
theorem finset.inv_smul_mem_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s : finset β} {a : α} {b : β} (ha : a ≠ 0) :
a⁻¹ • b ∈ s ↔ b ∈ a • s
source
theorem finset.mem_inv_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s : finset β} {a : α} {b : β} (ha : a ≠ 0) :
b ∈ a⁻¹ • s ↔ a • b ∈ s
source
@[simp]
theorem finset.smul_finset_subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a ≠ 0) :
a • s ⊆ a • t ↔ s ⊆ t
source
theorem finset.smul_finset_subset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a ≠ 0) :
a • s ⊆ t ↔ s ⊆ a⁻¹ • t
source
theorem finset.subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a ≠ 0) :
s ⊆ a • t ↔ a⁻¹ • s ⊆ t
source
theorem finset.smul_finset_inter₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a ≠ 0) :
a • (s ∩ t) = a • s ∩ a • t
source
theorem finset.smul_finset_sdiff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a ≠ 0) :
a • (s \ t) = a • s \ a • t
source
theorem finset.smul_finset_symm_diff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a ≠ 0) :
a • s ∆ t = (a • s) ∆ (a • t)
source
theorem finset.smul_univ₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] [fintype β] {s : finset α} (hs : ¬s ⊆ 0) :
s • finset.univ = finset.univ
source
theorem finset.smul_finset_univ₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {a : α} [fintype β] (ha : a ≠ 0) :
a • finset.univ = finset.univ

Note that we have neither smul_with_zero α (finset β) nor smul_with_zero (finset α) (finset β) because 0 * ∅ ≠ 0.

source
theorem finset.smul_zero_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] (s : finset α) :
s • 0 ⊆ 0
source
theorem finset.zero_smul_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] (t : finset β) :
0 • t ⊆ 0
source
theorem finset.nonempty.smul_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset α} (hs : s.nonempty) :
s • 0 = 0
source
theorem finset.nonempty.zero_smul {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {t : finset β} (ht : t.nonempty) :
0 • t = 0
source
theorem finset.zero_smul_finset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset β} (h : s.nonempty) :
0 • s = 0

A nonempty set is scaled by zero to the singleton set containing 0.

source
theorem finset.zero_smul_finset_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] (s : finset β) :
0 • s ⊆ 0
source
theorem finset.zero_mem_smul_finset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {t : finset β} {a : α} (h : 0 ∈ t) :
0 ∈ a • t
source
theorem finset.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset α} {t : finset β} [no_zero_smul_divisors α β] :
0 ∈ s • t ↔ 0 ∈ s ∧ t.nonempty ∨ 0 ∈ t ∧ s.nonempty
source
theorem finset.zero_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {t : finset β} [no_zero_smul_divisors α β] {a : α} (ha : a ≠ 0) :
0 ∈ a • t ↔ 0 ∈ t
source
@[simp]
theorem finset.smul_finset_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] [decidable_eq β] (a : α) (t : finset β) :
a • -t = -(a • t)
source
@[protected, simp]
theorem finset.smul_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] [decidable_eq β] (s : finset α) (t : finset β) :
s • -t = -(s • t)
source
@[simp]
theorem finset.neg_smul_finset {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] [decidable_eq β] {t : finset β} {a : α} :
-a • t = -(a • t)
source
@[protected, simp]
theorem finset.neg_smul {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] [decidable_eq β] {s : finset α} {t : finset β} [decidable_eq α] :
-s • t = -(s • t)
source
@[simp]
theorem set.to_finset_zero {α : Type u_2} [has_zero α] :
0.to_finset = 0
source
@[simp]
theorem set.to_finset_one {α : Type u_2} [has_one α] :
1.to_finset = 1
source
@[simp]
theorem set.finite.to_finset_one {α : Type u_2} [has_one α] (h : 1.finite := set.finite_one) :
set.finite.to_finset h = 1
source
@[simp]
theorem set.finite.to_finset_zero {α : Type u_2} [has_zero α] (h : 0.finite := set.finite_zero) :
set.finite.to_finset h = 0
source
@[simp]
theorem set.to_finset_mul {α : Type u_2} [decidable_eq α] [has_mul α] (s t : set α) [fintype ↥s] [fintype ↥t] [fintype ↥(s * t)] :
(s * t).to_finset = s.to_finset * t.to_finset
source
@[simp]
theorem set.to_finset_add {α : Type u_2} [decidable_eq α] [has_add α] (s t : set α) [fintype ↥s] [fintype ↥t] [fintype ↥(s + t)] :
(s + t).to_finset = s.to_finset + t.to_finset
source
theorem set.finite.to_finset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : set α} (hs : s.finite) (ht : t.finite) (hf : (s * t).finite := _) :
set.finite.to_finset hf = hs.to_finset * ht.to_finset
source
theorem set.finite.to_finset_add {α : Type u_2} [decidable_eq α] [has_add α] {s t : set α} (hs : s.finite) (ht : t.finite) (hf : (s + t).finite := _) :
set.finite.to_finset hf = hs.to_finset + ht.to_finset
source
@[simp]
theorem set.to_finset_smul {α : Type u_2} {β : Type u_3} [has_smul α β] [decidable_eq β] (s : set α) (t : set β) [fintype ↥s] [fintype ↥t] [fintype ↥(s • t)] :
(s • t).to_finset = s.to_finset • t.to_finset
source
@[simp]
theorem set.to_finset_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] [decidable_eq β] (s : set α) (t : set β) [fintype ↥s] [fintype ↥t] [fintype ↥(s +ᵥ t)] :
(s +ᵥ t).to_finset = s.to_finset +ᵥ t.to_finset
source
theorem set.finite.to_finset_smul {α : Type u_2} {β : Type u_3} [has_smul α β] [decidable_eq β] {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) (hf : (s • t).finite := _) :
set.finite.to_finset hf = hs.to_finset • ht.to_finset
source
theorem set.finite.to_finset_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] [decidable_eq β] {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) (hf : (s +ᵥ t).finite := _) :
set.finite.to_finset hf = hs.to_finset +ᵥ ht.to_finset
source
@[simp]
theorem set.to_finset_smul_set {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) (s : set β) [fintype ↥s] [fintype ↥(a • s)] :
(a • s).to_finset = a • s.to_finset
source
@[simp]
theorem set.to_finset_vadd_set {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) (s : set β) [fintype ↥s] [fintype ↥(a +ᵥ s)] :
(a +ᵥ s).to_finset = a +ᵥ s.to_finset
source
theorem set.finite.to_finset_vadd_set {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {a : α} {s : set β} (hs : s.finite) (hf : (a +ᵥ s).finite := _) :
set.finite.to_finset hf = a +ᵥ hs.to_finset
source
theorem set.finite.to_finset_smul_set {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {a : α} {s : set β} (hs : s.finite) (hf : (a • s).finite := _) :
set.finite.to_finset hf = a • hs.to_finset
source
@[simp]
theorem set.to_finset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (s t : set β) [fintype ↥s] [fintype ↥t] [fintype ↥(s -ᵥ t)] :
(s -ᵥ t).to_finset = s.to_finset -ᵥ t.to_finset
source
theorem set.finite.to_finset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : set β} (hs : s.finite) (ht : t.finite) (hf : (s -ᵥ t).finite := _) :
set.finite.to_finset hf = hs.to_finset -ᵥ ht.to_finset