mathlib documentation

data.finset.pointwise

Pointwise operations of finsets #

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}.

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 sets #

source
@[protected, instance]
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, instance]
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]
theorem finset.coe_zero {α : Type u_2} [has_zero α] :
↑0 = 0
source
@[simp]
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}

Finset negation/inversion #

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

The pointwise inverse of a finset s: s⁻¹ = {x⁻¹ | x ∈ s}.

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

The pointwise negation of a finset s: -s = {-x | x ∈ s}.

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 inv_nonempty_iff.

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

Alias of 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, 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, instance]
def finset.has_add {α : Type u_2} [decidable_eq α] [has_add α] :
has_add (finset α)

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

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

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

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.product 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.product t)
source
theorem finset.add_image_prod {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst + x.snd) (s.product t) = s + t
source
theorem finset.image_mul_prod {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
finset.image (λ (x : α × α), (x.fst) * x.snd) (s.product 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 : α} (ha : a ∈ s) (hb : b ∈ t) :
a * b ∈ s * t
source
theorem finset.add_mem_add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} {a b : α} (ha : a ∈ s) (hb : b ∈ t) :
a + b ∈ s + t
source
theorem finset.add_card_le {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).card ≤ (s.card) * t.card
source
theorem finset.mul_card_le {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).card ≤ (s.card) * t.card
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.add_nonempty_iff {α : Type u_2} [decidable_eq α] [has_add α] (s t : finset α) :
(s + t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[simp]
theorem finset.mul_nonempty_iff {α : Type u_2} [decidable_eq α] [has_mul α] (s t : finset α) :
(s * t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem finset.add_subset_add {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁ + t₁ ⊆ s₂ + t₂
source
theorem finset.mul_subset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁ * t₁ ⊆ s₂ * t₂
source
@[simp]
theorem finset.mul_singleton {α : Type u_2} [decidable_eq α] [has_mul α] {s : finset α} (a : α) :
s * {a} = finset.image (λ (_x : α), _x * a) s
source
@[simp]
theorem finset.add_singleton {α : Type u_2} [decidable_eq α] [has_add α] {s : finset α} (a : α) :
s + {a} = finset.image (λ (_x : α), _x + a) s
source
@[simp]
theorem finset.singleton_add {α : Type u_2} [decidable_eq α] [has_add α] {s : finset α} (a : α) :
{a} + s = finset.image (has_add.add a) s
source
@[simp]
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.subset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {u : finset α} {s t : set α} (f : ↑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 α} (f : ↑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.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
source
@[simp]
theorem finset.image_mul_left {α : Type u_2} [group α] {t : finset α} {a : α} [decidable_eq α] :
finset.image (λ (b : α), a * b) t = t.preimage (λ (b : α), a⁻¹ * b) _
source
@[simp]
theorem finset.image_add_left {α : Type u_2} [add_group α] {t : finset α} {a : α} [decidable_eq α] :
finset.image (λ (b : α), a + b) t = t.preimage (λ (b : α), -a + b) _
source
@[simp]
theorem finset.image_mul_right {α : Type u_2} [group α] {t : finset α} {b : α} [decidable_eq α] :
finset.image (λ (_x : α), _x * b) t = t.preimage (λ (_x : α), _x * b⁻¹) _
source
@[simp]
theorem finset.image_add_right {α : Type u_2} [add_group α] {t : finset α} {b : α} [decidable_eq α] :
finset.image (λ (_x : α), _x + b) t = t.preimage (λ (_x : α), _x + -b) _
source
theorem finset.image_add_left' {α : Type u_2} [add_group α] {t : finset α} {a : α} [decidable_eq α] :
finset.image (λ (b : α), -a + b) t = t.preimage (λ (b : α), a + b) _
source
theorem finset.image_mul_left' {α : Type u_2} [group α] {t : finset α} {a : α} [decidable_eq α] :
finset.image (λ (b : α), a⁻¹ * b) t = t.preimage (λ (b : α), a * b) _
source
theorem finset.image_add_right' {α : Type u_2} [add_group α] {t : finset α} {b : α} [decidable_eq α] :
finset.image (λ (_x : α), _x + -b) t = t.preimage (λ (_x : α), _x + b) _
source
theorem finset.image_mul_right' {α : Type u_2} [group α] {t : finset α} {b : α} [decidable_eq α] :
finset.image (λ (_x : α), _x * b⁻¹) t = t.preimage (λ (_x : α), _x * b) _
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 (λ (b : α), a * b) _ = {a⁻¹}
source
@[simp]
theorem finset.preimage_add_left_zero {α : Type u_2} [add_group α] {a : α} :
0.preimage (λ (b : α), a + b) _ = {-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 (λ (b : α), -a + b) _ = {a}
source
theorem finset.preimage_mul_left_one' {α : Type u_2} [group α] {a : α} :
1.preimage (λ (b : α), a⁻¹ * b) _ = {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}

Finset subtraction/division #

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

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

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

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

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.product 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.product 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.product t) = s / t
source
theorem finset.mem_div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} {x : α} :
x ∈ s / t ↔ ∃ (y z : α), y ∈ s ∧ z ∈ t ∧ y / z = x
source
theorem finset.mem_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} {x : α} :
x ∈ s - t ↔ ∃ (y z : α), y ∈ s ∧ z ∈ t ∧ y - z = x
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 : α} (ha : a ∈ s) (hb : b ∈ t) :
a / b ∈ s / t
source
theorem finset.sub_mem_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} {a b : α} (ha : a ∈ s) (hb : 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_nonempty_iff {α : Type u_2} [decidable_eq α] [has_div α] (s t : finset α) :
(s / t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[simp]
theorem finset.sub_nonempty_iff {α : Type u_2} [decidable_eq α] [has_sub α] (s t : finset α) :
(s - t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem finset.div_subset_div {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁ / t₁ ⊆ s₂ / t₂
source
theorem finset.sub_subset_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁ - t₁ ⊆ s₂ - t₂
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.subset_sub {α : Type u_2} [decidable_eq α] [has_sub α] {u : finset α} {s t : set α} (f : ↑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 α} (f : ↑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.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

Instances #

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

Repeated pointwise addition (not the same as pointwise repeated addition!) of a finset.

Equations
source
@[protected, instance]
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.

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

Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a finset.

Equations
source
@[protected, instance]
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.

Equations
source
@[simp]
theorem finset.coe_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] (s : finset α) (n : ℕ) :
↑(n • s) = n • ↑s
source
@[simp]
theorem finset.coe_pow {α : Type u_2} [decidable_eq α] [monoid α] (s : finset α) (n : ℕ) :
↑(s ^ n) = ↑s ^ n
source
@[simp]
theorem finset.coe_zsmul {α : Type u_2} [decidable_eq α] [add_group α] (s : finset α) (n : ℤ) :
↑(n • s) = n • ↑s
source
@[simp]
theorem finset.coe_zpow {α : Type u_2} [decidable_eq α] [group α] (s : finset α) (n : ℤ) :
↑(s ^ n) = ↑s ^ n
source
@[simp]
theorem finset.coe_zpow' {α : Type u_2} [decidable_eq α] [group_with_zero α] (s : finset α) (n : ℤ) :
↑(s ^ n) = ↑s ^ n
source
@[protected, instance]
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, instance]
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
@[protected, instance]
def finset.semigroup {α : Type u_2} [decidable_eq α] [semigroup α] :
semigroup (finset α)

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

Equations
source
@[protected, instance]
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
@[protected, instance]
def finset.monoid {α : Type u_2} [decidable_eq α] [monoid α] :
monoid (finset α)

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

Equations
source
@[protected, instance]
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
@[protected, instance]
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, instance]
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
@[protected, instance]
def finset.sub_neg_add_monoid {α : Type u_2} [decidable_eq α] [add_group α] :
sub_neg_monoid (finset α)

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

Equations
source
@[protected, instance]
def finset.div_inv_monoid {α : Type u_2} [decidable_eq α] [group α] :
div_inv_monoid (finset α)

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

Equations
source
@[protected, instance]
def finset.div_inv_monoid' {α : Type u_2} [decidable_eq α] [group_with_zero α] :
div_inv_monoid (finset α)

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

Equations

Finset addition/multiplication #

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

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

Equations
source
@[protected, instance]
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_scalar α β] {s : finset α} {t : finset β} :
s • t = finset.image (λ (p : α × β), p.fst • p.snd) (s.product 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.product t)
source
theorem finset.image_smul_product {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {s : finset α} {t : finset β} :
finset.image (λ (x : α × β), x.fst • x.snd) (s.product 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.product t) = s +ᵥ t
source
theorem finset.mem_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {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_scalar α β] (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 : β} (ha : a ∈ s) (hb : b ∈ t) :
a +ᵥ b ∈ s +ᵥ t
source
theorem finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {s : finset α} {t : finset β} {a : α} {b : β} (ha : a ∈ s) (hb : 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_scalar α β] {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_scalar α β] (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_scalar α β] (s : finset α) :
s • ∅ = ∅
source
@[simp]
theorem finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {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_scalar α β] {s : finset α} {t : finset β} (hs : s.nonempty) (ht : t.nonempty) :
(s • t).nonempty
source
theorem finset.nonempty.vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} (hs : s.nonempty) (ht : t.nonempty) :
(s +ᵥ t).nonempty
source
theorem finset.smul_subset_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₁ ⊆ s₂) (ht : 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 β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂
source
@[simp]
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
@[simp]
theorem finset.smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {s : finset α} (b : β) :
s • {b} = finset.image (λ (_x : α), _x • b) s
source
@[simp]
theorem finset.singleton_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {t : finset β} (a : α) :
{a} • t = finset.image (has_scalar.smul a) t
source
@[simp]
theorem finset.singleton_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {t : finset β} (a : α) :
{a} +ᵥ t = finset.image (has_vadd.vadd a) t
source
@[simp]
theorem finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) (b : β) :
{a} +ᵥ {b} = {a +ᵥ b}
source
@[simp]
theorem finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] (a : α) (b : β) :
{a} • {b} = {a • b}
source
theorem finset.subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {u : finset β} {s : set α} {t : set β} (f : ↑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_scalar α β] {u : finset β} {s : set α} {t : set β} (f : ↑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'.

Finset addition/multiplication #

source
@[protected, instance]
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 (λ (p : β × β), p.fst -ᵥ p.snd) (s.product t)
source
theorem finset.image_vsub_product {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
finset.image (λ (x : β × β), x.fst -ᵥ x.snd) (s.product 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 : β} (hb : b ∈ s) (hc : 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_nonempty_iff {α : 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 β} (hs : s.nonempty) (ht : t.nonempty) :
(s -ᵥ t).nonempty
source
theorem finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t₁ t₂ : finset β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
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
@[simp]
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.subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : set β} {u : finset α} (f : ↑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, instance]
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, instance]
def finset.has_scalar_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] :
has_scalar α (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_scalar α β] {s : finset β} {a : α} :
a • s = finset.image (has_scalar.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_scalar α β] {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_scalar α β] {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_scalar α β] {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.vadd_finset_mem_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} {b : β} (hb : b ∈ s) :
a +ᵥ b ∈ a +ᵥ s
source
theorem finset.smul_finset_mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {s : finset β} {a : α} {b : β} (hb : 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_scalar α β] {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_scalar α β] (a : α) :
a • ∅ = ∅
source
@[simp]
theorem finset.smul_finset_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_scalar α β] {s : finset β} {a : α} :
(a • s).nonempty ↔ s.nonempty
source
@[simp]
theorem finset.vadd_finset_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {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_scalar α β] {s : finset β} {a : α} (hs : s.nonempty) :
(a • s).nonempty
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_scalar α β] {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_scalar α β] {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
@[protected, instance]
def finset.vadd_comm_class_set {α : 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_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
smul_comm_class α (finset β) (finset γ)
source
@[protected, instance]
def finset.smul_comm_class_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
smul_comm_class (finset α) β (finset γ)
source
@[protected, instance]
def finset.vadd_comm_class_set' {α : 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.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_scalar α γ] [has_scalar β γ] [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_scalar α β] [has_scalar α γ] [has_scalar β γ] [is_scalar_tower α β γ] :
is_scalar_tower α β (finset γ)
source
@[protected, instance]
def finset.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_scalar α β] [has_scalar α γ] [has_scalar β γ] [is_scalar_tower α β γ] :
is_scalar_tower α (finset β) (finset γ)
source
@[protected, instance]
def finset.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_scalar α β] [has_scalar α γ] [has_scalar β γ] [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_scalar α β] [has_scalar αᵐᵒᵖ β] [is_central_scalar α β] :
is_central_scalar α (finset β)