Pointwise operations of finsets

This file defines pointwise algebraic operations on finsets.

Main declarations

For finsets s and t:

• 0 (Finset.zero): The singleton {0}.
• 1 (Finset.one): The singleton {1}.
• -s (Finset.neg): Negation, finset of all -x where x ∈ s.
• s⁻¹ (Finset.inv): Inversion, finset of all x⁻¹ where x ∈ s.
• s + t (Finset.add): Addition, finset of all x + y where x ∈ s and y ∈ t.
• s * t (Finset.mul): Multiplication, finset of all x * y where x ∈ s and y ∈ t.
• s - t (Finset.sub): Subtraction, finset of all x - y where x ∈ s and y ∈ t.
• s / t (Finset.div): Division, finset of all x / y where x ∈ s and y ∈ 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

def Finset.one {α : Type u_2} [One α] : One (Finset α)

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

def Finset.zero {α : Type u_2} [Zero α] : Zero (Finset α)

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

@[simp]

theorem Finset.mem_one {α : Type u_2} [One α] {a : α} : a ∈ 1 ↔ a = 1

@[simp]

theorem Finset.mem_zero {α : Type u_2} [Zero α] {a : α} : a ∈ 0 ↔ a = 0

@[simp]

theorem Finset.coe_one {α : Type u_2} [One α] : ↑1 = 1

@[simp]

theorem Finset.coe_zero {α : Type u_2} [Zero α] : ↑0 = 0

@[simp]

theorem Finset.coe_eq_one {α : Type u_2} [One α] {s : Finset α} : ↑s = 1 ↔ s = 1

@[simp]

theorem Finset.coe_eq_zero {α : Type u_2} [Zero α] {s : Finset α} : ↑s = 0 ↔ s = 0

@[simp]

theorem Finset.one_subset {α : Type u_2} [One α] {s : Finset α} : 1 ⊆ s ↔ 1 ∈ s

@[simp]

theorem Finset.zero_subset {α : Type u_2} [Zero α] {s : Finset α} : 0 ⊆ s ↔ 0 ∈ s

theorem Finset.singleton_one {α : Type u_2} [One α] : {1} = 1

theorem Finset.singleton_zero {α : Type u_2} [Zero α] : {0} = 0

theorem Finset.one_mem_one {α : Type u_2} [One α] : 1 ∈ 1

theorem Finset.zero_mem_zero {α : Type u_2} [Zero α] : 0 ∈ 0

@[simp]

theorem Finset.one_nonempty {α : Type u_2} [One α] : Finset.Nonempty 1

@[simp]

theorem Finset.zero_nonempty {α : Type u_2} [Zero α] : Finset.Nonempty 0

@[simp]

theorem Finset.map_one {α : Type u_2} {β : Type u_3} [One α] {f : α ↪ β} : map f 1 = {f 1}

@[simp]

theorem Finset.map_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : α ↪ β} : map f 0 = {f 0}

@[simp]

theorem Finset.image_one {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] {f : α → β} : image f 1 = {f 1}

@[simp]

theorem Finset.image_zero {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] {f : α → β} : image f 0 = {f 0}

theorem Finset.subset_one_iff_eq {α : Type u_2} [One α] {s : Finset α} : s ⊆ 1 ↔ s = ∅ ∨ s = 1

theorem Finset.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : Finset α} : s ⊆ 0 ↔ s = ∅ ∨ s = 0

theorem Finset.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Finset α} (h : s.Nonempty) : s ⊆ 1 ↔ s = 1

theorem Finset.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : Finset α} (h : s.Nonempty) : s ⊆ 0 ↔ s = 0

@[simp]

theorem Finset.card_one {α : Type u_2} [One α] : card 1 = 1

@[simp]

theorem Finset.card_zero {α : Type u_2} [Zero α] : card 0 = 1

def Finset.singletonOneHom {α : Type u_2} [One α] : OneHom α (Finset α)

The singleton operation as a OneHom.

def Finset.singletonZeroHom {α : Type u_2} [Zero α] : ZeroHom α (Finset α)

The singleton operation as a ZeroHom.

@[simp]

theorem Finset.coe_singletonOneHom {α : Type u_2} [One α] : ⇑singletonOneHom = singleton

@[simp]

theorem Finset.coe_singletonZeroHom {α : Type u_2} [Zero α] : ⇑singletonZeroHom = singleton

@[simp]

theorem Finset.singletonOneHom_apply {α : Type u_2} [One α] (a : α) : singletonOneHom a = {a}

@[simp]

theorem Finset.singletonZeroHom_apply {α : Type u_2} [Zero α] (a : α) : singletonZeroHom a = {a}

def Finset.imageOneHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) : OneHom (Finset α) (Finset β)

Lift a OneHom to Finset via image.

def Finset.imageZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [FunLike F α β] [ZeroHomClass F α β] (f : F) : ZeroHom (Finset α) (Finset β)

Lift a ZeroHom to Finset via image

@[simp]

theorem Finset.imageZeroHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [FunLike F α β] [ZeroHomClass F α β] (f : F) (s : Finset α) : (imageZeroHom f) s = image (⇑f) s

@[simp]

theorem Finset.imageOneHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) (s : Finset α) : (imageOneHom f) s = image (⇑f) s

@[simp]

theorem Finset.sup_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeSup β] [OrderBot β] (f : α → β) : sup 1 f = f 1

@[simp]

theorem Finset.sup_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeSup β] [OrderBot β] (f : α → β) : sup 0 f = f 0

@[simp]

theorem Finset.sup'_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeSup β] (f : α → β) : sup' 1 ⋯ f = f 1

@[simp]

theorem Finset.sup'_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeSup β] (f : α → β) : sup' 0 ⋯ f = f 0

@[simp]

theorem Finset.inf_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeInf β] [OrderTop β] (f : α → β) : inf 1 f = f 1

@[simp]

theorem Finset.inf_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeInf β] [OrderTop β] (f : α → β) : inf 0 f = f 0

@[simp]

theorem Finset.inf'_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeInf β] (f : α → β) : inf' 1 ⋯ f = f 1

@[simp]

theorem Finset.inf'_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeInf β] (f : α → β) : inf' 0 ⋯ f = f 0

@[simp]

theorem Finset.max_one {α : Type u_2} [One α] [LinearOrder α] : Finset.max 1 = 1

@[simp]

theorem Finset.max_zero {α : Type u_2} [Zero α] [LinearOrder α] : Finset.max 0 = 0

@[simp]

theorem Finset.min_one {α : Type u_2} [One α] [LinearOrder α] : Finset.min 1 = 1

@[simp]

theorem Finset.min_zero {α : Type u_2} [Zero α] [LinearOrder α] : Finset.min 0 = 0

@[simp]

theorem Finset.max'_one {α : Type u_2} [One α] [LinearOrder α] : max' 1 ⋯ = 1

@[simp]

theorem Finset.max'_zero {α : Type u_2} [Zero α] [LinearOrder α] : max' 0 ⋯ = 0

@[simp]

theorem Finset.min'_one {α : Type u_2} [One α] [LinearOrder α] : min' 1 ⋯ = 1

@[simp]

theorem Finset.min'_zero {α : Type u_2} [Zero α] [LinearOrder α] : min' 0 ⋯ = 0

@[simp]

theorem Finset.image_op_one {α : Type u_2} [One α] [DecidableEq α] : image MulOpposite.op 1 = 1

@[simp]

theorem Finset.image_op_zero {α : Type u_2} [Zero α] [DecidableEq α] : image AddOpposite.op 0 = 0

@[simp]

theorem Finset.map_op_one {α : Type u_2} [One α] : map MulOpposite.opEquiv.toEmbedding 1 = 1

@[simp]

theorem Finset.map_op_zero {α : Type u_2} [Zero α] : map AddOpposite.opEquiv.toEmbedding 0 = 0

@[simp]

theorem Finset.one_product_one {α : Type u_2} {β : Type u_3} [One α] [One β] : 1 ×ˢ 1 = 1

@[simp]

theorem Finset.zero_product_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] : 0 ×ˢ 0 = 0

Finset negation/inversion

def Finset.inv {α : Type u_2} [DecidableEq α] [Inv α] : Inv (Finset α)

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

def Finset.neg {α : Type u_2} [DecidableEq α] [Neg α] : Neg (Finset α)

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

theorem Finset.inv_def {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹ = image (fun (x : α) => x⁻¹) s

theorem Finset.neg_def {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : -s = image (fun (x : α) => -x) s

theorem Finset.image_inv_eq_inv {α : Type u_2} [DecidableEq α] [Inv α] (s : Finset α) : image (fun (x : α) => x⁻¹) s = s⁻¹

theorem Finset.image_neg_eq_neg {α : Type u_2} [DecidableEq α] [Neg α] (s : Finset α) : image (fun (x : α) => -x) s = -s

theorem Finset.mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {x : α} : x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x

theorem Finset.mem_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {x : α} : x ∈ -s ↔ ∃ y ∈ s, -y = x

theorem Finset.inv_mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {a : α} (ha : a ∈ s) : a⁻¹ ∈ s⁻¹

theorem Finset.neg_mem_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {a : α} (ha : a ∈ s) : -a ∈ -s

theorem Finset.card_inv_le {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹.card ≤ s.card

theorem Finset.card_neg_le {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : (-s).card ≤ s.card

@[simp]

theorem Finset.inv_empty {α : Type u_2} [DecidableEq α] [Inv α] : ∅⁻¹ = ∅

@[simp]

theorem Finset.neg_empty {α : Type u_2} [DecidableEq α] [Neg α] : -∅ = ∅

@[simp]

theorem Finset.inv_nonempty_iff {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹.Nonempty ↔ s.Nonempty

@[simp]

theorem Finset.neg_nonempty_iff {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : (-s).Nonempty ↔ s.Nonempty

theorem Finset.Nonempty.inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s.Nonempty → s⁻¹.Nonempty

Alias of the reverse direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹.Nonempty → s.Nonempty

Alias of the forward direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : (-s).Nonempty → s.Nonempty

theorem Finset.Nonempty.neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : s.Nonempty → (-s).Nonempty

@[simp]

theorem Finset.inv_eq_empty {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹ = ∅ ↔ s = ∅

@[simp]

theorem Finset.neg_eq_empty {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : -s = ∅ ↔ s = ∅

theorem Finset.inv_subset_inv {α : Type u_2} [DecidableEq α] [Inv α] {s t : Finset α} (h : s ⊆ t) : s⁻¹ ⊆ t⁻¹

theorem Finset.neg_subset_neg {α : Type u_2} [DecidableEq α] [Neg α] {s t : Finset α} (h : s ⊆ t) : -s ⊆ -t

@[simp]

theorem Finset.inv_singleton {α : Type u_2} [DecidableEq α] [Inv α] (a : α) : {a}⁻¹ = {a⁻¹}

@[simp]

theorem Finset.neg_singleton {α : Type u_2} [DecidableEq α] [Neg α] (a : α) : -{a} = {-a}

@[simp]

theorem Finset.inv_insert {α : Type u_2} [DecidableEq α] [Inv α] (a : α) (s : Finset α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹

@[simp]

theorem Finset.neg_insert {α : Type u_2} [DecidableEq α] [Neg α] (a : α) (s : Finset α) : -insert a s = insert (-a) (-s)

@[simp]

theorem Finset.sup_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : s⁻¹.sup f = s.sup fun (x : α) => f x⁻¹

@[simp]

theorem Finset.sup_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : (-s).sup f = s.sup fun (x : α) => f (-x)

@[simp]

theorem Finset.sup'_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeSup β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) : s⁻¹.sup' hs f = s.sup' ⋯ fun (x : α) => f x⁻¹

@[simp]

theorem Finset.sup'_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeSup β] {s : Finset α} (hs : (-s).Nonempty) (f : α → β) : (-s).sup' hs f = s.sup' ⋯ fun (x : α) => f (-x)

@[simp]

theorem Finset.inf_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) : s⁻¹.inf f = s.inf fun (x : α) => f x⁻¹

@[simp]

theorem Finset.inf_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) : (-s).inf f = s.inf fun (x : α) => f (-x)

@[simp]

theorem Finset.inf'_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeInf β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) : s⁻¹.inf' hs f = s.inf' ⋯ fun (x : α) => f x⁻¹

@[simp]

theorem Finset.inf'_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeInf β] {s : Finset α} (hs : (-s).Nonempty) (f : α → β) : (-s).inf' hs f = s.inf' ⋯ fun (x : α) => f (-x)

theorem Finset.image_op_inv {α : Type u_2} [DecidableEq α] [Inv α] (s : Finset α) : image MulOpposite.op s⁻¹ = (image MulOpposite.op s)⁻¹

theorem Finset.image_op_neg {α : Type u_2} [DecidableEq α] [Neg α] (s : Finset α) : image AddOpposite.op (-s) = -image AddOpposite.op s

theorem Finset.map_op_inv {α : Type u_2} [DecidableEq α] [Inv α] (s : Finset α) : map MulOpposite.opEquiv.toEmbedding s⁻¹ = (map MulOpposite.opEquiv.toEmbedding s)⁻¹

theorem Finset.map_op_neg {α : Type u_2} [DecidableEq α] [Neg α] (s : Finset α) : map AddOpposite.opEquiv.toEmbedding (-s) = -map AddOpposite.opEquiv.toEmbedding s

@[simp]

theorem Finset.mem_inv' {α : Type u_2} [DecidableEq α] [InvolutiveInv α] {s : Finset α} {a : α} : a ∈ s⁻¹ ↔ a⁻¹ ∈ s

@[simp]

theorem Finset.mem_neg' {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] {s : Finset α} {a : α} : a ∈ -s ↔ -a ∈ s

@[simp]

theorem Finset.coe_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : ↑s⁻¹ = (↑s)⁻¹

@[simp]

theorem Finset.coe_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : ↑(-s) = -↑s

@[simp]

theorem Finset.card_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : s⁻¹.card = s.card

@[simp]

theorem Finset.card_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : (-s).card = s.card

@[simp]

theorem Finset.preimage_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : s.preimage (fun (x : α) => x⁻¹) ⋯ = s⁻¹

@[simp]

theorem Finset.preimage_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : s.preimage (fun (x : α) => -x) ⋯ = -s

@[simp]

theorem Finset.inv_univ {α : Type u_2} [DecidableEq α] [InvolutiveInv α] [Fintype α] : univ⁻¹ = univ

@[simp]

theorem Finset.neg_univ {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] [Fintype α] : -univ = univ

@[simp]

theorem Finset.inv_inter {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s t : Finset α) : (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹

@[simp]

theorem Finset.neg_inter {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s t : Finset α) : -(s ∩ t) = -s ∩ -t

@[simp]

theorem Finset.inv_product {α : Type u_2} {β : Type u_3} [DecidableEq α] [InvolutiveInv α] [DecidableEq β] [InvolutiveInv β] (s : Finset α) (t : Finset β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹

@[simp]

theorem Finset.neg_product {α : Type u_2} {β : Type u_3} [DecidableEq α] [InvolutiveNeg α] [DecidableEq β] [InvolutiveNeg β] (s : Finset α) (t : Finset β) : -s ×ˢ t = (-s) ×ˢ (-t)

Finset addition/multiplication

def Finset.mul {α : Type u_2} [DecidableEq α] [Mul α] : Mul (Finset α)

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

def Finset.add {α : Type u_2} [DecidableEq α] [Add α] : Add (Finset α)

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

theorem Finset.mul_def {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : s * t = image (fun (p : α × α) => p.1 * p.2) (s ×ˢ t)

theorem Finset.add_def {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : s + t = image (fun (p : α × α) => p.1 + p.2) (s ×ˢ t)

theorem Finset.image_mul_product {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : image (fun (x : α × α) => x.1 * x.2) (s ×ˢ t) = s * t

theorem Finset.image_add_product {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : image (fun (x : α × α) => x.1 + x.2) (s ×ˢ t) = s + t

theorem Finset.mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} {x : α} : x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

theorem Finset.mem_add {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} {x : α} : x ∈ s + t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x

@[simp]

theorem Finset.coe_mul {α : Type u_2} [DecidableEq α] [Mul α] (s t : Finset α) : ↑(s * t) = ↑s * ↑t

@[simp]

theorem Finset.coe_add {α : Type u_2} [DecidableEq α] [Add α] (s t : Finset α) : ↑(s + t) = ↑s + ↑t

theorem Finset.mul_mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} {a b : α} : a ∈ s → b ∈ t → a * b ∈ s * t

theorem Finset.add_mem_add {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} {a b : α} : a ∈ s → b ∈ t → a + b ∈ s + t

theorem Finset.card_mul_le {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : (s * t).card ≤ s.card * t.card

theorem Finset.card_add_le {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : (s + t).card ≤ s.card * t.card

theorem Finset.card_mul_iff {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : (s * t).card = s.card * t.card ↔ Set.InjOn (fun (p : α × α) => p.1 * p.2) (↑s ×ˢ ↑t)

theorem Finset.card_add_iff {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : (s + t).card = s.card * t.card ↔ Set.InjOn (fun (p : α × α) => p.1 + p.2) (↑s ×ˢ ↑t)

@[simp]

theorem Finset.empty_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) : ∅ * s = ∅

@[simp]

theorem Finset.empty_add {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) : ∅ + s = ∅

@[simp]

theorem Finset.mul_empty {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) : s * ∅ = ∅

@[simp]

theorem Finset.add_empty {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) : s + ∅ = ∅

@[simp]

theorem Finset.mul_eq_empty {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : s * t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.add_eq_empty {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : s + t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.mul_nonempty {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Finset.add_nonempty {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : (s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Finset.Nonempty.mul {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : s.Nonempty → t.Nonempty → (s * t).Nonempty

theorem Finset.Nonempty.add {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : s.Nonempty → t.Nonempty → (s + t).Nonempty

theorem Finset.Nonempty.of_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : (s * t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_add_left {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : (s + t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s t : Finset α} : (s * t).Nonempty → t.Nonempty

theorem Finset.Nonempty.of_add_right {α : Type u_2} [DecidableEq α] [Add α] {s t : Finset α} : (s + t).Nonempty → t.Nonempty

@[simp]

theorem Finset.singleton_mul_singleton {α : Type u_2} [DecidableEq α] [Mul α] (a b : α) : {a} * {b} = {a * b}

@[simp]

theorem Finset.singleton_add_singleton {α : Type u_2} [DecidableEq α] [Add α] (a b : α) : {a} + {b} = {a + b}

theorem Finset.mul_subset_mul {α : Type u_2} [DecidableEq α] [Mul α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ * t₁ ⊆ s₂ * t₂

theorem Finset.add_subset_add {α : Type u_2} [DecidableEq α] [Add α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ + t₁ ⊆ s₂ + t₂

theorem Finset.mul_subset_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s t₁ t₂ : Finset α} : t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂

theorem Finset.add_subset_add_left {α : Type u_2} [DecidableEq α] [Add α] {s t₁ t₂ : Finset α} : t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂

theorem Finset.mul_subset_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s₁ s₂ t : Finset α} : s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t

theorem Finset.add_subset_add_right {α : Type u_2} [DecidableEq α] [Add α] {s₁ s₂ t : Finset α} : s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t

instance Finset.instMulLeftMono {α : Type u_2} [DecidableEq α] [Mul α] : MulLeftMono (Finset α)

instance Finset.instAddLeftMono {α : Type u_2} [DecidableEq α] [Add α] : AddLeftMono (Finset α)

instance Finset.instMulRightMono {α : Type u_2} [DecidableEq α] [Mul α] : MulRightMono (Finset α)

instance Finset.instAddRightMono {α : Type u_2} [DecidableEq α] [Add α] : AddRightMono (Finset α)

theorem Finset.mul_subset_iff {α : Type u_2} [DecidableEq α] [Mul α] {s t u : Finset α} : s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u

theorem Finset.add_subset_iff {α : Type u_2} [DecidableEq α] [Add α] {s t u : Finset α} : s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u

theorem Finset.union_mul {α : Type u_2} [DecidableEq α] [Mul α] {s₁ s₂ t : Finset α} : (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t

theorem Finset.union_add {α : Type u_2} [DecidableEq α] [Add α] {s₁ s₂ t : Finset α} : s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)

theorem Finset.mul_union {α : Type u_2} [DecidableEq α] [Mul α] {s t₁ t₂ : Finset α} : s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂

theorem Finset.add_union {α : Type u_2} [DecidableEq α] [Add α] {s t₁ t₂ : Finset α} : s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)

theorem Finset.inter_mul_subset {α : Type u_2} [DecidableEq α] [Mul α] {s₁ s₂ t : Finset α} : s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)

theorem Finset.inter_add_subset {α : Type u_2} [DecidableEq α] [Add α] {s₁ s₂ t : Finset α} : s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)

theorem Finset.mul_inter_subset {α : Type u_2} [DecidableEq α] [Mul α] {s t₁ t₂ : Finset α} : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)

theorem Finset.add_inter_subset {α : Type u_2} [DecidableEq α] [Add α] {s t₁ t₂ : Finset α} : s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)

theorem Finset.inter_mul_union_subset_union {α : Type u_2} [DecidableEq α] [Mul α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

theorem Finset.inter_add_union_subset_union {α : Type u_2} [DecidableEq α] [Add α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)

theorem Finset.union_mul_inter_subset_union {α : Type u_2} [DecidableEq α] [Mul α] {s₁ s₂ t₁ t₂ : Finset α} : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

theorem Finset.union_add_inter_subset_union {α : Type u_2} [DecidableEq α] [Add α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)

theorem Finset.subset_mul {α : Type u_2} [DecidableEq α] [Mul α] {u : Finset α} {s t : Set α} : ↑u ⊆ s * t → ∃ (s' : Finset α) (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'.

theorem Finset.subset_add {α : Type u_2} [DecidableEq α] [Add α] {u : Finset α} {s t : Set α} : ↑u ⊆ s + t → ∃ (s' : Finset α) (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'.

theorem Finset.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) {s t : Finset α} [DecidableEq β] : image (⇑f) (s * t) = image (⇑f) s * image (⇑f) t

theorem Finset.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) {s t : Finset α} [DecidableEq β] : image (⇑f) (s + t) = image (⇑f) s + image (⇑f) t

theorem Finset.image_op_mul {α : Type u_2} [DecidableEq α] [Mul α] (s t : Finset α) : image MulOpposite.op (s * t) = image MulOpposite.op t * image MulOpposite.op s

theorem Finset.image_op_add {α : Type u_2} [DecidableEq α] [Add α] (s t : Finset α) : image AddOpposite.op (s + t) = image AddOpposite.op t + image AddOpposite.op s

@[simp]

theorem Finset.product_mul_product_comm {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [Mul β] [DecidableEq β] (s₁ s₂ : Finset α) (t₁ t₂ : Finset β) : s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

@[simp]

theorem Finset.product_add_product_comm {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [Add β] [DecidableEq β] (s₁ s₂ : Finset α) (t₁ t₂ : Finset β) : s₁ ×ˢ t₁ + s₂ ×ˢ t₂ = (s₁ + s₂) ×ˢ (t₁ + t₂)

theorem Finset.map_op_mul {α : Type u_2} [DecidableEq α] [Mul α] (s t : Finset α) : map MulOpposite.opEquiv.toEmbedding (s * t) = map MulOpposite.opEquiv.toEmbedding t * map MulOpposite.opEquiv.toEmbedding s

theorem Finset.map_op_add {α : Type u_2} [DecidableEq α] [Add α] (s t : Finset α) : map AddOpposite.opEquiv.toEmbedding (s + t) = map AddOpposite.opEquiv.toEmbedding t + map AddOpposite.opEquiv.toEmbedding s

def Finset.singletonMulHom {α : Type u_2} [DecidableEq α] [Mul α] : α →ₙ* Finset α

The singleton operation as a MulHom.

def Finset.singletonAddHom {α : Type u_2} [DecidableEq α] [Add α] : α →ₙ+ Finset α

The singleton operation as an AddHom.

@[simp]

theorem Finset.coe_singletonMulHom {α : Type u_2} [DecidableEq α] [Mul α] : ⇑singletonMulHom = singleton

@[simp]

theorem Finset.coe_singletonAddHom {α : Type u_2} [DecidableEq α] [Add α] : ⇑singletonAddHom = singleton

@[simp]

theorem Finset.singletonMulHom_apply {α : Type u_2} [DecidableEq α] [Mul α] (a : α) : singletonMulHom a = {a}

@[simp]

theorem Finset.singletonAddHom_apply {α : Type u_2} [DecidableEq α] [Add α] (a : α) : singletonAddHom a = {a}

def Finset.imageMulHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) [DecidableEq β] : Finset α →ₙ* Finset β

Lift a MulHom to Finset via image.

def Finset.imageAddHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) [DecidableEq β] : Finset α →ₙ+ Finset β

Lift an AddHom to Finset via image

@[simp]

theorem Finset.imageMulHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) [DecidableEq β] (s : Finset α) : (imageMulHom f) s = image (⇑f) s

@[simp]

theorem Finset.imageAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) [DecidableEq β] (s : Finset α) : (imageAddHom f) s = image (⇑f) s

@[simp]

theorem Finset.sup_mul_le {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s * t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a

@[simp]

theorem Finset.sup_add_le {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s + t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x + y) ≤ a

theorem Finset.sup_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s * t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x * x_1)

theorem Finset.sup_add_left {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s + t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x + x_1)

theorem Finset.sup_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s * t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x * y)

theorem Finset.sup_add_right {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s + t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x + y)

@[simp]

theorem Finset.le_inf_mul {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} : a ≤ (s * t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)

@[simp]

theorem Finset.le_inf_add {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} : a ≤ (s + t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x + y)

theorem Finset.inf_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s * t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x * x_1)

theorem Finset.inf_add_left {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s + t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x + x_1)

theorem Finset.inf_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s * t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x * y)

theorem Finset.inf_add_right {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s + t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x + y)

Finset subtraction/division

def Finset.div {α : Type u_2} [DecidableEq α] [Div α] : Div (Finset α)

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

def Finset.sub {α : Type u_2} [DecidableEq α] [Sub α] : Sub (Finset α)

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

theorem Finset.div_def {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : s / t = image (fun (p : α × α) => p.1 / p.2) (s ×ˢ t)

theorem Finset.sub_def {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : s - t = image (fun (p : α × α) => p.1 - p.2) (s ×ˢ t)

theorem Finset.image_div_product {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : image (fun (x : α × α) => x.1 / x.2) (s ×ˢ t) = s / t

theorem Finset.image_sub_product {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : image (fun (x : α × α) => x.1 - x.2) (s ×ˢ t) = s - t

theorem Finset.mem_div {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} {a : α} : a ∈ s / t ↔ ∃ b ∈ s, ∃ c ∈ t, b / c = a

theorem Finset.mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} {a : α} : a ∈ s - t ↔ ∃ b ∈ s, ∃ c ∈ t, b - c = a

@[simp]

theorem Finset.coe_div {α : Type u_2} [DecidableEq α] [Div α] (s t : Finset α) : ↑(s / t) = ↑s / ↑t

@[simp]

theorem Finset.coe_sub {α : Type u_2} [DecidableEq α] [Sub α] (s t : Finset α) : ↑(s - t) = ↑s - ↑t

theorem Finset.div_mem_div {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} {a b : α} : a ∈ s → b ∈ t → a / b ∈ s / t

theorem Finset.sub_mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} {a b : α} : a ∈ s → b ∈ t → a - b ∈ s - t

theorem Finset.div_card_le {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : (s / t).card ≤ s.card * t.card

theorem Finset.sub_card_le {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : (s - t).card ≤ s.card * t.card

@[simp]

theorem Finset.empty_div {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) : ∅ / s = ∅

@[simp]

theorem Finset.empty_sub {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) : ∅ - s = ∅

@[simp]

theorem Finset.div_empty {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) : s / ∅ = ∅

@[simp]

theorem Finset.sub_empty {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) : s - ∅ = ∅

@[simp]

theorem Finset.div_eq_empty {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : s / t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.sub_eq_empty {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : s - t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.div_nonempty {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Finset.sub_nonempty {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : (s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Finset.Nonempty.div {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : s.Nonempty → t.Nonempty → (s / t).Nonempty

theorem Finset.Nonempty.sub {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : s.Nonempty → t.Nonempty → (s - t).Nonempty

theorem Finset.Nonempty.of_div_left {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : (s / t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : (s - t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_div_right {α : Type u_2} [DecidableEq α] [Div α] {s t : Finset α} : (s / t).Nonempty → t.Nonempty

theorem Finset.Nonempty.of_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s t : Finset α} : (s - t).Nonempty → t.Nonempty

@[simp]

theorem Finset.div_singleton {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) : s / {a} = image (fun (x : α) => x / a) s

@[simp]

theorem Finset.sub_singleton {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} (a : α) : s - {a} = image (fun (x : α) => x - a) s

@[simp]

theorem Finset.singleton_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) : {a} / s = image (fun (x : α) => a / x) s

@[simp]

theorem Finset.singleton_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} (a : α) : {a} - s = image (fun (x : α) => a - x) s

theorem Finset.singleton_div_singleton {α : Type u_2} [DecidableEq α] [Div α] (a b : α) : {a} / {b} = {a / b}

theorem Finset.singleton_sub_singleton {α : Type u_2} [DecidableEq α] [Sub α] (a b : α) : {a} - {b} = {a - b}

theorem Finset.div_subset_div {α : Type u_2} [DecidableEq α] [Div α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ / t₁ ⊆ s₂ / t₂

theorem Finset.sub_subset_sub {α : Type u_2} [DecidableEq α] [Sub α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ - t₁ ⊆ s₂ - t₂

theorem Finset.div_subset_div_left {α : Type u_2} [DecidableEq α] [Div α] {s t₁ t₂ : Finset α} : t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂

theorem Finset.sub_subset_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s t₁ t₂ : Finset α} : t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂

theorem Finset.div_subset_div_right {α : Type u_2} [DecidableEq α] [Div α] {s₁ s₂ t : Finset α} : s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t

theorem Finset.sub_subset_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s₁ s₂ t : Finset α} : s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t

theorem Finset.div_subset_iff {α : Type u_2} [DecidableEq α] [Div α] {s t u : Finset α} : s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u

theorem Finset.sub_subset_iff {α : Type u_2} [DecidableEq α] [Sub α] {s t u : Finset α} : s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u

theorem Finset.union_div {α : Type u_2} [DecidableEq α] [Div α] {s₁ s₂ t : Finset α} : (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t

theorem Finset.union_sub {α : Type u_2} [DecidableEq α] [Sub α] {s₁ s₂ t : Finset α} : s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)

theorem Finset.div_union {α : Type u_2} [DecidableEq α] [Div α] {s t₁ t₂ : Finset α} : s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂

theorem Finset.sub_union {α : Type u_2} [DecidableEq α] [Sub α] {s t₁ t₂ : Finset α} : s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)

theorem Finset.inter_div_subset {α : Type u_2} [DecidableEq α] [Div α] {s₁ s₂ t : Finset α} : s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)

theorem Finset.inter_sub_subset {α : Type u_2} [DecidableEq α] [Sub α] {s₁ s₂ t : Finset α} : s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)

theorem Finset.div_inter_subset {α : Type u_2} [DecidableEq α] [Div α] {s t₁ t₂ : Finset α} : s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)

theorem Finset.sub_inter_subset {α : Type u_2} [DecidableEq α] [Sub α] {s t₁ t₂ : Finset α} : s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)

theorem Finset.inter_div_union_subset_union {α : Type u_2} [DecidableEq α] [Div α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

theorem Finset.inter_sub_union_subset_union {α : Type u_2} [DecidableEq α] [Sub α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)

theorem Finset.union_div_inter_subset_union {α : Type u_2} [DecidableEq α] [Div α] {s₁ s₂ t₁ t₂ : Finset α} : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

theorem Finset.union_sub_inter_subset_union {α : Type u_2} [DecidableEq α] [Sub α] {s₁ s₂ t₁ t₂ : Finset α} : s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)

theorem Finset.subset_div {α : Type u_2} [DecidableEq α] [Div α] {u : Finset α} {s t : Set α} : ↑u ⊆ s / t → ∃ (s' : Finset α) (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'.

theorem Finset.subset_sub {α : Type u_2} [DecidableEq α] [Sub α] {u : Finset α} {s t : Set α} : ↑u ⊆ s - t → ∃ (s' : Finset α) (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'.

@[simp]

theorem Finset.sup_div_le {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s / t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a

@[simp]

theorem Finset.sup_sub_le {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s - t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x - y) ≤ a

theorem Finset.sup_div_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s / t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x / x_1)

theorem Finset.sup_sub_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s - t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x - x_1)

theorem Finset.sup_div_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s / t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x / y)

theorem Finset.sup_sub_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s - t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x - y)

@[simp]

theorem Finset.le_inf_div {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} : a ≤ (s / t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y)

@[simp]

theorem Finset.le_inf_sub {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} : a ≤ (s - t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x - y)

theorem Finset.inf_div_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s / t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x / x_1)

theorem Finset.inf_sub_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s - t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x - x_1)

theorem Finset.inf_div_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s / t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x / y)

theorem Finset.inf_sub_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : (s - t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x - y)

Instances

def Finset.nsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] : SMul ℕ (Finset α)

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

def Finset.npow {α : Type u_2} [DecidableEq α] [One α] [Mul α] : Pow (Finset α) ℕ

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

def Finset.zsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] [Neg α] : SMul ℤ (Finset α)

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

def Finset.zpow {α : Type u_2} [DecidableEq α] [One α] [Mul α] [Inv α] : Pow (Finset α) ℤ

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

def Finset.semigroup {α : Type u_2} [DecidableEq α] [Semigroup α] : Semigroup (Finset α)

Finset α is a Semigroup under pointwise operations if α is.

def Finset.addSemigroup {α : Type u_2} [DecidableEq α] [AddSemigroup α] : AddSemigroup (Finset α)

Finset α is an AddSemigroup under pointwise operations if α is.

def Finset.commSemigroup {α : Type u_2} [DecidableEq α] [CommSemigroup α] : CommSemigroup (Finset α)

Finset α is a CommSemigroup under pointwise operations if α is.

def Finset.addCommSemigroup {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] : AddCommSemigroup (Finset α)

Finset α is an AddCommSemigroup under pointwise operations if α is.

theorem Finset.inter_mul_union_subset {α : Type u_2} [DecidableEq α] [CommSemigroup α] {s t : Finset α} : s ∩ t * (s ∪ t) ⊆ s * t

theorem Finset.inter_add_union_subset {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] {s t : Finset α} : s ∩ t + (s ∪ t) ⊆ s + t

theorem Finset.union_mul_inter_subset {α : Type u_2} [DecidableEq α] [CommSemigroup α] {s t : Finset α} : (s ∪ t) * (s ∩ t) ⊆ s * t

theorem Finset.union_add_inter_subset {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] {s t : Finset α} : s ∪ t + s ∩ t ⊆ s + t

def Finset.mulOneClass {α : Type u_2} [DecidableEq α] [MulOneClass α] : MulOneClass (Finset α)

Finset α is a MulOneClass under pointwise operations if α is.

def Finset.addZeroClass {α : Type u_2} [DecidableEq α] [AddZeroClass α] : AddZeroClass (Finset α)

Finset α is an AddZeroClass under pointwise operations if α is.

theorem Finset.subset_mul_left {α : Type u_2} [DecidableEq α] [MulOneClass α] (s : Finset α) {t : Finset α} (ht : 1 ∈ t) : s ⊆ s * t

theorem Finset.subset_add_left {α : Type u_2} [DecidableEq α] [AddZeroClass α] (s : Finset α) {t : Finset α} (ht : 0 ∈ t) : s ⊆ s + t

theorem Finset.subset_mul_right {α : Type u_2} [DecidableEq α] [MulOneClass α] {s : Finset α} (t : Finset α) (hs : 1 ∈ s) : t ⊆ s * t

theorem Finset.subset_add_right {α : Type u_2} [DecidableEq α] [AddZeroClass α] {s : Finset α} (t : Finset α) (hs : 0 ∈ s) : t ⊆ s + t

def Finset.singletonMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : α →* Finset α

The singleton operation as a MonoidHom.

def Finset.singletonAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : α →+ Finset α

The singleton operation as an AddMonoidHom.

@[simp]

theorem Finset.coe_singletonMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : ⇑singletonMonoidHom = singleton

@[simp]

theorem Finset.coe_singletonAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : ⇑singletonAddMonoidHom = singleton

@[simp]

theorem Finset.singletonMonoidHom_apply {α : Type u_2} [DecidableEq α] [MulOneClass α] (a : α) : singletonMonoidHom a = {a}

@[simp]

theorem Finset.singletonAddMonoidHom_apply {α : Type u_2} [DecidableEq α] [AddZeroClass α] (a : α) : singletonAddMonoidHom a = {a}

noncomputable def Finset.coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : Finset α →* Set α

The coercion from Finset to Set as a MonoidHom.

noncomputable def Finset.coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : Finset α →+ Set α

The coercion from Finset to set as an AddMonoidHom.

@[simp]

theorem Finset.coe_coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : ⇑coeMonoidHom = toSet

@[simp]

theorem Finset.coe_coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : ⇑coeAddMonoidHom = toSet

@[simp]

theorem Finset.coeMonoidHom_apply {α : Type u_2} [DecidableEq α] [MulOneClass α] (s : Finset α) : coeMonoidHom s = ↑s

@[simp]

theorem Finset.coeAddMonoidHom_apply {α : Type u_2} [DecidableEq α] [AddZeroClass α] (s : Finset α) : coeAddMonoidHom s = ↑s

def Finset.imageMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) : Finset α →* Finset β

Lift a MonoidHom to Finset via image.

def Finset.imageAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) : Finset α →+ Finset β

Lift an add_monoid_hom to Finset via image

@[simp]

theorem Finset.imageMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (a✝ : Finset α) : (imageMonoidHom f) a✝ = (imageMulHom f).toFun a✝

@[simp]

theorem Finset.imageAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (a✝ : Finset α) : (imageAddMonoidHom f) a✝ = (imageAddHom f).toFun a✝

@[simp]

theorem Finset.coe_pow {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (n : ℕ) : ↑(s ^ n) = ↑s ^ n

@[simp]

theorem Finset.coe_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

noncomputable def Finset.monoid {α : Type u_2} [DecidableEq α] [Monoid α] : Monoid (Finset α)

Finset α is a Monoid under pointwise operations if α is.

noncomputable def Finset.addMonoid {α : Type u_2} [DecidableEq α] [AddMonoid α] : AddMonoid (Finset α)

Finset α is an AddMonoid under pointwise operations if α is.

theorem Finset.pow_right_monotone {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} (hs : 1 ∈ s) : Monotone fun (x : ℕ) => s ^ x

theorem Finset.nsmul_right_monotone {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} (hs : 0 ∈ s) : Monotone fun (x : ℕ) => x • s

theorem Finset.pow_subset_pow_left {α : Type u_2} [DecidableEq α] [Monoid α] {s t : Finset α} {n : ℕ} (hst : s ⊆ t) : s ^ n ⊆ t ^ n

theorem Finset.nsmul_subset_nsmul_left {α : Type u_2} [DecidableEq α] [AddMonoid α] {s t : Finset α} {n : ℕ} (hst : s ⊆ t) : n • s ⊆ n • t

theorem Finset.pow_subset_pow_right {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {m n : ℕ} (hs : 1 ∈ s) (hmn : m ≤ n) : s ^ m ⊆ s ^ n

theorem Finset.nsmul_subset_nsmul_right {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {m n : ℕ} (hs : 0 ∈ s) (hmn : m ≤ n) : m • s ⊆ n • s

theorem Finset.pow_subset_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s t : Finset α} {m n : ℕ} (hst : s ⊆ t) (ht : 1 ∈ t) (hmn : m ≤ n) : s ^ m ⊆ t ^ n

theorem Finset.nsmul_subset_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s t : Finset α} {m n : ℕ} (hst : s ⊆ t) (ht : 0 ∈ t) (hmn : m ≤ n) : m • s ⊆ n • t

theorem Finset.subset_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n

theorem Finset.subset_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {n : ℕ} (hs : 0 ∈ s) (hn : n ≠ 0) : s ⊆ n • s

@[deprecated Finset.pow_subset_pow_right (since := "2024-11-19")]

theorem Finset.pow_subset_pow_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {m n : ℕ} (hs : 1 ∈ s) (hmn : m ≤ n) : s ^ m ⊆ s ^ n

Alias of Finset.pow_subset_pow_right.

@[deprecated Finset.nsmul_subset_nsmul_right (since := "2024-11-19")]

theorem Finset.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {m n : ℕ} (hs : 0 ∈ s) (hmn : m ≤ n) : m • s ⊆ n • s

Alias of Finset.nsmul_subset_nsmul_right.

theorem Finset.pow_subset_pow_mul_of_sq_subset_mul {α : Type u_2} [DecidableEq α] [Monoid α] {s t : Finset α} {n : ℕ} (hst : s ^ 2 ⊆ t * s) (hn : n ≠ 0) : s ^ n ⊆ t ^ (n - 1) * s

theorem Finset.nsmul_subset_nsmul_add_of_sq_subset_add {α : Type u_2} [DecidableEq α] [AddMonoid α] {s t : Finset α} {n : ℕ} (hst : 2 • s ⊆ t + s) (hn : n ≠ 0) : n • s ⊆ (n - 1) • t + s

@[simp]

theorem Finset.empty_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} (hn : n ≠ 0) : ∅ ^ n = ∅

@[simp]

theorem Finset.nsmul_empty {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} (hn : n ≠ 0) : n • ∅ = ∅

theorem Finset.Nonempty.pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} (hs : s.Nonempty) {n : ℕ} : (s ^ n).Nonempty

theorem Finset.Nonempty.nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} (hs : s.Nonempty) {n : ℕ} : (n • s).Nonempty

@[simp]

theorem Finset.pow_eq_empty {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : ℕ} : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

@[simp]

theorem Finset.nsmul_eq_empty {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {n : ℕ} : n • s = ∅ ↔ s = ∅ ∧ n ≠ 0

@[simp]

theorem Finset.singleton_pow {α : Type u_2} [DecidableEq α] [Monoid α] (a : α) (n : ℕ) : {a} ^ n = {a ^ n}

@[simp]

theorem Finset.nsmul_singleton {α : Type u_2} [DecidableEq α] [AddMonoid α] (a : α) (n : ℕ) : n • {a} = {n • a}

theorem Finset.pow_mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} {n : ℕ} (ha : a ∈ s) : a ^ n ∈ s ^ n

theorem Finset.nsmul_mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} {n : ℕ} (ha : a ∈ s) : n • a ∈ n • s

theorem Finset.one_mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : ℕ} (hs : 1 ∈ s) : 1 ∈ s ^ n

theorem Finset.zero_mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {n : ℕ} (hs : 0 ∈ s) : 0 ∈ n • s

theorem Finset.inter_pow_subset {α : Type u_2} [DecidableEq α] [Monoid α] {s t : Finset α} {n : ℕ} : (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

theorem Finset.inter_nsmul_subset {α : Type u_2} [DecidableEq α] [AddMonoid α] {s t : Finset α} {n : ℕ} : n • (s ∩ t) ⊆ n • s ∩ n • t

@[simp]

theorem Finset.coe_list_prod {α : Type u_2} [DecidableEq α] [Monoid α] (s : List (Finset α)) : ↑s.prod = (List.map toSet s).prod

@[simp]

theorem Finset.coe_list_sum {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : List (Finset α)) : ↑s.sum = (List.map toSet s).sum

theorem Finset.mem_prod_list_ofFn {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} {a : α} {s : Fin n → Finset α} : a ∈ (List.ofFn s).prod ↔ ∃ (f : (i : Fin n) → { x : α // x ∈ s i }), (List.ofFn fun (i : Fin n) => ↑(f i)).prod = a

theorem Finset.mem_sum_list_ofFn {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Finset α} : a ∈ (List.ofFn s).sum ↔ ∃ (f : (i : Fin n) → { x : α // x ∈ s i }), (List.ofFn fun (i : Fin n) => ↑(f i)).sum = a

theorem Finset.mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ (f : Fin n → { x : α // x ∈ s }), (List.ofFn fun (i : Fin n) => ↑(f i)).prod = a

theorem Finset.mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} {n : ℕ} : a ∈ n • s ↔ ∃ (f : Fin n → { x : α // x ∈ s }), (List.ofFn fun (i : Fin n) => ↑(f i)).sum = a

theorem Finset.card_pow_le {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : ℕ} : (s ^ n).card ≤ s.card ^ n

theorem Finset.card_nsmul_le {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {n : ℕ} : (n • s).card ≤ s.card ^ n

theorem Finset.mul_univ_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} [Fintype α] (hs : 1 ∈ s) : s * univ = univ

theorem Finset.add_univ_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} [Fintype α] (hs : 0 ∈ s) : s + univ = univ

theorem Finset.univ_mul_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {t : Finset α} [Fintype α] (ht : 1 ∈ t) : univ * t = univ

theorem Finset.univ_add_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {t : Finset α} [Fintype α] (ht : 0 ∈ t) : univ + t = univ

@[simp]

theorem Finset.univ_mul_univ {α : Type u_2} [DecidableEq α] [Monoid α] [Fintype α] : univ * univ = univ

@[simp]

theorem Finset.univ_add_univ {α : Type u_2} [DecidableEq α] [AddMonoid α] [Fintype α] : univ + univ = univ

@[simp]

theorem Finset.univ_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} [Fintype α] (hn : n ≠ 0) : univ ^ n = univ

@[simp]

theorem Finset.nsmul_univ {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} [Fintype α] (hn : n ≠ 0) : n • univ = univ

theorem IsUnit.finset {α : Type u_2} [DecidableEq α] [Monoid α] {a : α} : IsUnit a → IsUnit {a}

theorem IsAddUnit.finset {α : Type u_2} [DecidableEq α] [AddMonoid α] {a : α} : IsAddUnit a → IsAddUnit {a}

theorem Finset.image_op_pow {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (n : ℕ) : image MulOpposite.op (s ^ n) = image MulOpposite.op s ^ n

theorem Finset.image_op_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ℕ) : image AddOpposite.op (n • s) = n • image AddOpposite.op s

theorem Finset.map_op_pow {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (n : ℕ) : map MulOpposite.opEquiv.toEmbedding (s ^ n) = map MulOpposite.opEquiv.toEmbedding s ^ n

theorem Finset.map_op_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ℕ) : map AddOpposite.opEquiv.toEmbedding (n • s) = n • map AddOpposite.opEquiv.toEmbedding s

theorem Finset.product_pow {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] (s : Finset α) (t : Finset β) (n : ℕ) : s ×ˢ t ^ n = (s ^ n) ×ˢ (t ^ n)

theorem Finset.product_nsmul {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddMonoid α] [AddMonoid β] (s : Finset α) (t : Finset β) (n : ℕ) : n • s ×ˢ t = (n • s) ×ˢ (n • t)

noncomputable def Finset.commMonoid {α : Type u_2} [DecidableEq α] [CommMonoid α] : CommMonoid (Finset α)

Finset α is a CommMonoid under pointwise operations if α is.

noncomputable def Finset.addCommMonoid {α : Type u_2} [DecidableEq α] [AddCommMonoid α] : AddCommMonoid (Finset α)

Finset α is an AddCommMonoid under pointwise operations if α is.

@[simp]

theorem Finset.coe_zpow {α : Type u_2} [DecidableEq α] [DivisionMonoid α] (s : Finset α) (n : ℤ) : ↑(s ^ n) = ↑s ^ n

@[simp]

theorem Finset.coe_zsmul {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ℤ) : ↑(n • s) = n • ↑s

theorem Finset.mul_eq_one_iff {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s t : Finset α} : s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

theorem Finset.add_eq_zero_iff {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s t : Finset α} : s + t = 0 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a + b = 0

noncomputable def Finset.divisionMonoid {α : Type u_2} [DecidableEq α] [DivisionMonoid α] : DivisionMonoid (Finset α)

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

noncomputable def Finset.subtractionMonoid {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] : SubtractionMonoid (Finset α)

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

@[simp]

theorem Finset.isUnit_iff {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} : IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a

@[simp]

theorem Finset.isAddUnit_iff {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} : IsAddUnit s ↔ ∃ (a : α), s = {a} ∧ IsAddUnit a

@[simp]

theorem Finset.isUnit_coe {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} : IsUnit ↑s ↔ IsUnit s

@[simp]

theorem Finset.isAddUnit_coe {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} : IsAddUnit ↑s ↔ IsAddUnit s

@[simp]

theorem Finset.univ_div_univ {α : Type u_2} [DecidableEq α] [DivisionMonoid α] [Fintype α] : univ / univ = univ

@[simp]

theorem Finset.univ_sub_univ {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] [Fintype α] : univ - univ = univ

theorem Finset.subset_div_left {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s t : Finset α} (ht : 1 ∈ t) : s ⊆ s / t

theorem Finset.subset_sub_left {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s t : Finset α} (ht : 0 ∈ t) : s ⊆ s - t

theorem Finset.inv_subset_div_right {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s t : Finset α} (hs : 1 ∈ s) : t⁻¹ ⊆ s / t

theorem Finset.neg_subset_sub_right {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s t : Finset α} (hs : 0 ∈ s) : -t ⊆ s - t

@[simp]

theorem Finset.empty_zpow {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {n : ℤ} (hn : n ≠ 0) : ∅ ^ n = ∅

@[simp]

theorem Finset.zsmul_empty {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {n : ℤ} (hn : n ≠ 0) : n • ∅ = ∅

theorem Finset.Nonempty.zpow {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} (hs : s.Nonempty) {n : ℤ} : (s ^ n).Nonempty

theorem Finset.Nonempty.zsmul {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} (hs : s.Nonempty) {n : ℤ} : (n • s).Nonempty

@[simp]

theorem Finset.zpow_eq_empty {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} {n : ℤ} : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

@[simp]

theorem Finset.zsmul_eq_empty {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} {n : ℤ} : n • s = ∅ ↔ s = ∅ ∧ n ≠ 0

@[simp]

theorem Finset.singleton_zpow {α : Type u_2} [DecidableEq α] [DivisionMonoid α] (a : α) (n : ℤ) : {a} ^ n = {a ^ n}

@[simp]

theorem Finset.zsmul_singleton {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] (a : α) (n : ℤ) : n • {a} = {n • a}

noncomputable def Finset.divisionCommMonoid {α : Type u_2} [DecidableEq α] [DivisionCommMonoid α] : DivisionCommMonoid (Finset α)

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

noncomputable def Finset.subtractionCommMonoid {α : Type u_2} [DecidableEq α] [SubtractionCommMonoid α] : SubtractionCommMonoid (Finset α)

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

Note that Finset is not a Group because s / s ≠ 1 in general.

@[simp]

theorem Finset.one_mem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s t : Finset α} : 1 ∈ s / t ↔ ¬Disjoint s t

@[simp]

theorem Finset.zero_mem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s t : Finset α} : 0 ∈ s - t ↔ ¬Disjoint s t

@[simp]

theorem Finset.one_mem_inv_mul_iff {α : Type u_2} [DecidableEq α] [Group α] {s t : Finset α} : 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t

@[simp]

theorem Finset.zero_mem_neg_add_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s t : Finset α} : 0 ∈ -t + s ↔ ¬Disjoint s t

theorem Finset.one_notMem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s t : Finset α} : 1 ∉ s / t ↔ Disjoint s t

theorem Finset.zero_notMem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s t : Finset α} : 0 ∉ s - t ↔ Disjoint s t

@[deprecated Finset.zero_notMem_sub_iff (since := "2025-05-23")]

theorem Finset.not_zero_mem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s t : Finset α} : 0 ∉ s - t ↔ Disjoint s t

Alias of Finset.zero_notMem_sub_iff.

@[deprecated Finset.one_notMem_div_iff (since := "2025-05-23")]

theorem Finset.not_one_mem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s t : Finset α} : 1 ∉ s / t ↔ Disjoint s t

Alias of Finset.one_notMem_div_iff.

theorem Finset.one_notMem_inv_mul_iff {α : Type u_2} [DecidableEq α] [Group α] {s t : Finset α} : 1 ∉ t⁻¹ * s ↔ Disjoint s t

theorem Finset.zero_notMem_neg_add_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s t : Finset α} : 0 ∉ -t + s ↔ Disjoint s t

@[deprecated Finset.zero_notMem_neg_add_iff (since := "2025-05-23")]

theorem Finset.not_zero_mem_neg_add_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s t : Finset α} : 0 ∉ -t + s ↔ Disjoint s t

Alias of Finset.zero_notMem_neg_add_iff.

@[deprecated Finset.one_notMem_inv_mul_iff (since := "2025-05-23")]

theorem Finset.not_one_mem_inv_mul_iff {α : Type u_2} [DecidableEq α] [Group α] {s t : Finset α} : 1 ∉ t⁻¹ * s ↔ Disjoint s t

Alias of Finset.one_notMem_inv_mul_iff.

theorem Finset.Nonempty.one_mem_div {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} (h : s.Nonempty) : 1 ∈ s / s

theorem Finset.Nonempty.zero_mem_sub {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} (h : s.Nonempty) : 0 ∈ s - s

theorem Finset.isUnit_singleton {α : Type u_2} [DecidableEq α] [Group α] (a : α) : IsUnit {a}

theorem Finset.isAddUnit_singleton {α : Type u_2} [DecidableEq α] [AddGroup α] (a : α) : IsAddUnit {a}

theorem Finset.isUnit_iff_singleton {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} : IsUnit s ↔ ∃ (a : α), s = {a}

@[simp]

theorem Finset.isUnit_iff_singleton_aux {α : Type u_5} [Group α] {s : Finset α} : (∃ (a : α), s = {a} ∧ IsUnit a) ↔ ∃ (a : α), s = {a}

@[simp]

theorem Finset.image_mul_left {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} : image (fun (b : α) => a * b) t = t.preimage (fun (b : α) => a⁻¹ * b) ⋯

@[simp]

theorem Finset.image_add_left {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} : image (fun (b : α) => a + b) t = t.preimage (fun (b : α) => -a + b) ⋯

@[simp]

theorem Finset.image_mul_right {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} : image (fun (x : α) => x * b) t = t.preimage (fun (x : α) => x * b⁻¹) ⋯

@[simp]

theorem Finset.image_add_right {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} : image (fun (x : α) => x + b) t = t.preimage (fun (x : α) => x + -b) ⋯

theorem Finset.image_mul_left' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} : image (fun (b : α) => a⁻¹ * b) t = t.preimage (fun (b : α) => a * b) ⋯

theorem Finset.image_add_left' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} : image (fun (b : α) => -a + b) t = t.preimage (fun (b : α) => a + b) ⋯

theorem Finset.image_mul_right' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} : image (fun (x : α) => x * b⁻¹) t = t.preimage (fun (x : α) => x * b) ⋯

theorem Finset.image_add_right' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} : image (fun (x : α) => x + -b) t = t.preimage (fun (x : α) => x + b) ⋯

theorem Finset.image_inv {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Finset α) : image (⇑f) s⁻¹ = (image (⇑f) s)⁻¹

theorem Finset.image_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Finset α) : image (⇑f) (-s) = -image (⇑f) s

theorem Finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) {s t : Finset α} : image (⇑f) (s / t) = image (⇑f) s / image (⇑f) t

@[simp]

theorem Finset.preimage_mul_left_singleton {α : Type u_2} [Group α] {a b : α} : {b}.preimage (fun (x : α) => a * x) ⋯ = {a⁻¹ * b}

@[simp]

theorem Finset.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a b : α} : {b}.preimage (fun (x : α) => a + x) ⋯ = {-a + b}

@[simp]

theorem Finset.preimage_mul_right_singleton {α : Type u_2} [Group α] {a b : α} : {b}.preimage (fun (x : α) => x * a) ⋯ = {b * a⁻¹}

@[simp]

theorem Finset.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a b : α} : {b}.preimage (fun (x : α) => x + a) ⋯ = {b + -a}

@[simp]

theorem Finset.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} : preimage 1 (fun (x : α) => a * x) ⋯ = {a⁻¹}

@[simp]

theorem Finset.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} : preimage 0 (fun (x : α) => a + x) ⋯ = {-a}

@[simp]

theorem Finset.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} : preimage 1 (fun (x : α) => x * b) ⋯ = {b⁻¹}

@[simp]

theorem Finset.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} : preimage 0 (fun (x : α) => x + b) ⋯ = {-b}

theorem Finset.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} : preimage 1 (fun (x : α) => a⁻¹ * x) ⋯ = {a}

theorem Finset.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} : preimage 0 (fun (x : α) => -a + x) ⋯ = {a}

theorem Finset.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} : preimage 1 (fun (x : α) => x * b⁻¹) ⋯ = {b}

theorem Finset.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} : preimage 0 (fun (x : α) => x + -b) ⋯ = {b}

theorem Finset.image_pow_of_ne_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] [FunLike F α β] [MulHomClass F α β] {n : ℕ} : n ≠ 0 → ∀ (f : F) (s : Finset α), image (⇑f) (s ^ n) = image (⇑f) s ^ n

theorem Finset.image_nsmul_of_ne_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddHomClass F α β] {n : ℕ} : n ≠ 0 → ∀ (f : F) (s : Finset α), image (⇑f) (n • s) = n • image (⇑f) s

theorem Finset.image_pow {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Finset α) (n : ℕ) : image (⇑f) (s ^ n) = image (⇑f) s ^ n

theorem Finset.image_nsmul {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Finset α) (n : ℕ) : image (⇑f) (n • s) = n • image (⇑f) s

theorem Finset.Nontrivial.mul_left {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] {s t : Finset α} : t.Nontrivial → s.Nonempty → (s * t).Nontrivial

theorem Finset.Nontrivial.add_left {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] {s t : Finset α} : t.Nontrivial → s.Nonempty → (s + t).Nontrivial

theorem Finset.Nontrivial.mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] {s t : Finset α} (hs : s.Nontrivial) (ht : t.Nontrivial) : (s * t).Nontrivial

theorem Finset.Nontrivial.add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] {s t : Finset α} (hs : s.Nontrivial) (ht : t.Nontrivial) : (s + t).Nontrivial

@[simp]

theorem Finset.card_singleton_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] (a : α) (t : Finset α) : ({a} * t).card = t.card

@[simp]

theorem Finset.card_singleton_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] (a : α) (t : Finset α) : ({a} + t).card = t.card

theorem Finset.singleton_mul_inter {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] (a : α) (s t : Finset α) : {a} * (s ∩ t) = {a} * s ∩ ({a} * t)

theorem Finset.singleton_add_inter {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] (a : α) (s t : Finset α) : {a} + s ∩ t = ({a} + s) ∩ ({a} + t)

theorem Finset.card_le_card_mul_left {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] {t s : Finset α} (hs : s.Nonempty) : t.card ≤ (s * t).card

theorem Finset.card_le_card_add_left {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] {t s : Finset α} (hs : s.Nonempty) : t.card ≤ (s + t).card

theorem Finset.card_le_card_mul_self {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] {s : Finset α} : s.card ≤ (s * s).card

The size of s * s is at least the size of s, version with left-cancellative multiplication. See card_le_card_mul_self' for the version with right-cancellative multiplication.

theorem Finset.card_le_card_add_self {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] {s : Finset α} : s.card ≤ (s + s).card

The size of s + s is at least the size of s, version with left-cancellative addition. See card_le_card_add_self' for the version with right-cancellative addition.

theorem Finset.Nontrivial.mul_right {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] {s t : Finset α} : s.Nontrivial → t.Nonempty → (s * t).Nontrivial

theorem Finset.Nontrivial.add_right {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] {s t : Finset α} : s.Nontrivial → t.Nonempty → (s + t).Nontrivial

@[simp]

theorem Finset.card_mul_singleton {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] (s : Finset α) (a : α) : (s * {a}).card = s.card

@[simp]

theorem Finset.card_add_singleton {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] (s : Finset α) (a : α) : (s + {a}).card = s.card

theorem Finset.inter_mul_singleton {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] (s t : Finset α) (a : α) : s ∩ t * {a} = s * {a} ∩ (t * {a})

theorem Finset.inter_add_singleton {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] (s t : Finset α) (a : α) : s ∩ t + {a} = (s + {a}) ∩ (t + {a})

theorem Finset.card_le_card_mul_right {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s.card ≤ (s * t).card

theorem Finset.card_le_card_add_right {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s.card ≤ (s + t).card

theorem Finset.card_le_card_mul_self' {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] {s : Finset α} : s.card ≤ (s * s).card

The size of s * s is at least the size of s, version with right-cancellative multiplication. See card_le_card_mul_self for the version with left-cancellative multiplication.

theorem Finset.card_le_card_add_self' {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] {s : Finset α} : s.card ≤ (s + s).card

The size of s + s is at least the size of s, version with right-cancellative addition. See card_le_card_add_self for the version with left-cancellative addition.

theorem Finset.Nontrivial.pow {α : Type u_2} [DecidableEq α] [CancelMonoid α] {s : Finset α} (hs : s.Nontrivial) {n : ℕ} : n ≠ 0 → (s ^ n).Nontrivial

theorem Finset.Nontrivial.nsmul {α : Type u_2} [DecidableEq α] [AddCancelMonoid α] {s : Finset α} (hs : s.Nontrivial) {n : ℕ} : n ≠ 0 → (n • s).Nontrivial

theorem Finset.Nonempty.card_pow_mono {α : Type u_2} [DecidableEq α] [CancelMonoid α] {s : Finset α} (hs : s.Nonempty) : Monotone fun (n : ℕ) => (s ^ n).card

See Finset.card_pow_mono for a version that works for the empty set.

theorem Finset.Nonempty.card_nsmul_mono {α : Type u_2} [DecidableEq α] [AddCancelMonoid α] {s : Finset α} (hs : s.Nonempty) : Monotone fun (n : ℕ) => (n • s).card

See Finset.card_nsmul_mono for a version that works for the empty set.

theorem Finset.card_pow_mono {α : Type u_2} [DecidableEq α] [CancelMonoid α] {s : Finset α} {m n : ℕ} (hm : m ≠ 0) (hmn : m ≤ n) : (s ^ m).card ≤ (s ^ n).card

See Finset.Nonempty.card_pow_mono for a version that works for zero powers.

theorem Finset.card_nsmul_mono {α : Type u_2} [DecidableEq α] [AddCancelMonoid α] {s : Finset α} {m n : ℕ} (hm : m ≠ 0) (hmn : m ≤ n) : (m • s).card ≤ (n • s).card

See Finset.Nonempty.card_nsmul_mono for a version that works for zero scalars.

theorem Finset.card_le_card_pow {α : Type u_2} [DecidableEq α] [CancelMonoid α] {s : Finset α} {n : ℕ} (hn : n ≠ 0) : s.card ≤ (s ^ n).card

theorem Finset.card_le_card_nsmul {α : Type u_2} [DecidableEq α] [AddCancelMonoid α] {s : Finset α} {n : ℕ} (hn : n ≠ 0) : s.card ≤ (n • s).card

theorem Finset.card_le_card_div_left {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) : t.card ≤ (s / t).card

theorem Finset.card_le_card_sub_left {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) : t.card ≤ (s - t).card

theorem Finset.card_le_card_div_right {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s.card ≤ (s / t).card

theorem Finset.card_le_card_sub_right {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s.card ≤ (s - t).card

theorem Finset.card_le_card_div_self {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.card ≤ (s / s).card

theorem Finset.card_le_card_sub_self {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : s.card ≤ (s - s).card

theorem Fintype.piFinset_mul {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Mul (α i)] (s t : (i : ι) → Finset (α i)) : (piFinset fun (i : ι) => s i * t i) = piFinset s * piFinset t

theorem Fintype.piFinset_add {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Add (α i)] (s t : (i : ι) → Finset (α i)) : (piFinset fun (i : ι) => s i + t i) = piFinset s + piFinset t

theorem Fintype.piFinset_div {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Div (α i)] (s t : (i : ι) → Finset (α i)) : (piFinset fun (i : ι) => s i / t i) = piFinset s / piFinset t

theorem Fintype.piFinset_sub {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Sub (α i)] (s t : (i : ι) → Finset (α i)) : (piFinset fun (i : ι) => s i - t i) = piFinset s - piFinset t

@[simp]

theorem Fintype.piFinset_inv {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Inv (α i)] (s : (i : ι) → Finset (α i)) : (piFinset fun (i : ι) => (s i)⁻¹) = (piFinset s)⁻¹

@[simp]

theorem Fintype.piFinset_neg {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Neg (α i)] (s : (i : ι) → Finset (α i)) : (piFinset fun (i : ι) => -s i) = -piFinset s

instance Set.instFintypeOne {α : Type u_2} [One α] : Fintype ↑1

instance Set.instFintypeZero {α : Type u_2} [Zero α] : Fintype ↑0

@[simp]

theorem Set.toFinset_one {α : Type u_2} [One α] : toFinset 1 = 1

@[simp]

theorem Set.toFinset_zero {α : Type u_2} [Zero α] : toFinset 0 = 0

@[simp]

theorem Set.Finite.toFinset_one {α : Type u_2} [One α] (h : Set.Finite 1 := ⋯) : Finite.toFinset h = 1

@[simp]

theorem Set.Finite.toFinset_zero {α : Type u_2} [Zero α] (h : Set.Finite 0 := ⋯) : Finite.toFinset h = 0

@[simp]

theorem Set.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] (s t : Set α) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s * t)] : (s * t).toFinset = s.toFinset * t.toFinset

@[simp]

theorem Set.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] (s t : Set α) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s + t)] : (s + t).toFinset = s.toFinset + t.toFinset

theorem Set.Finite.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] {s t : Set α} (hs : s.Finite) (ht : t.Finite) (hf : (s * t).Finite := ⋯) : Finite.toFinset hf = hs.toFinset * ht.toFinset

theorem Set.Finite.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] {s t : Set α} (hs : s.Finite) (ht : t.Finite) (hf : (s + t).Finite := ⋯) : Finite.toFinset hf = hs.toFinset + ht.toFinset