@[reducible, inline]

abbrev Set.IsMulBasisOfOrder {α : Type u_1} [CommMonoid α] (A : Set α) (n : ℕ) : Prop

A set A : Set α is a multiplicative basis of order n if for any element a : α, it can be expressed as a product of n elements lying in A.

Equations

• A.IsMulBasisOfOrder n = ∀ (a : α), a ∈ A ^ n

@[reducible, inline]

abbrev Set.IsAddBasisOfOrder {α : Type u_1} [AddCommMonoid α] (A : Set α) (n : ℕ) : Prop

A set A : Set α is an additive basis of order n if for any element a : α, it can be expressed as a sum of n elements lying in A.

Equations

• A.IsAddBasisOfOrder n = ∀ (a : α), a ∈ n • A

@[reducible, inline]

abbrev Set.IsMulBasis {α : Type u_1} [CommMonoid α] (A : Set α) : Prop

A multiplicative basis of some order.

Equations

• A.IsMulBasis = ∃ (n : ℕ), A.IsMulBasisOfOrder n

@[reducible, inline]

abbrev Set.IsAddBasis {α : Type u_1} [AddCommMonoid α] (A : Set α) : Prop

An additive basis of some order

Equations

• A.IsAddBasis = ∃ (n : ℕ), A.IsAddBasisOfOrder n

theorem Set.IsMulBasisOfOrder.toMulBasis {α : Type u_1} [CommMonoid α] {A : Set α} {n : ℕ} (hA : A.IsMulBasisOfOrder n) : A.IsMulBasis

theorem Set.IsAddBasisOfOrder.toAddBasis {α : Type u_1} [AddCommMonoid α] {A : Set α} {n : ℕ} (hA : A.IsAddBasisOfOrder n) : A.IsAddBasis

theorem Set.isMulBasisOfOrder_iff {α : Type u_1} [CommMonoid α] (A : Set α) (n : ℕ) : A.IsMulBasisOfOrder n ↔ ∀ (a : α), ∃ (f : Fin n → α) (_ : ∀ (i : Fin n), f i ∈ A), ∏ i : Fin n, f i = a

theorem Set.isAddBasisOfOrder_iff {α : Type u_1} [AddCommMonoid α] (A : Set α) (n : ℕ) : A.IsAddBasisOfOrder n ↔ ∀ (a : α), ∃ (f : Fin n → α) (_ : ∀ (i : Fin n), f i ∈ A), ∑ i : Fin n, f i = a

theorem Set.isMulBasisOfOrder_two_iff {α : Type u_1} [CommMonoid α] (A : Set α) : A.IsMulBasisOfOrder 2 ↔ ∀ (a : α), a ∈ A * A

A set A : Set α is a multiplicative basis of order 2 if every a : α belongs to A + A.

theorem Set.isAddBasisOfOrder_two_iff {α : Type u_1} [AddCommMonoid α] (A : Set α) : A.IsAddBasisOfOrder 2 ↔ ∀ (a : α), a ∈ A + A

A set A : Set α is an additive basis of order 2 if every a : α belongs to A + A.

theorem Set.not_isMulBasisOfOrder_zero {α : Type u_1} [CommMonoid α] [Nontrivial α] [DecidableEq α] (A : Set α) : ¬A.IsMulBasisOfOrder 0

No set is a multiplicative basis of order 0.

theorem Set.not_isAddBasisOfOrder_zero {α : Type u_1} [AddCommMonoid α] [Nontrivial α] [DecidableEq α] (A : Set α) : ¬A.IsAddBasisOfOrder 0

No set is an additive basis of order 0.

theorem Set.isMulBasisOfOrder_one_iff {α : Type u_1} [CommMonoid α] (A : Set α) : A.IsMulBasisOfOrder 1 ↔ A = univ

theorem Set.isAddBasisOfOrder_zero_iff {α : Type u_1} [AddCommMonoid α] (A : Set α) : A.IsAddBasisOfOrder 1 ↔ A = univ

@[reducible, inline]

abbrev Set.IsAsymptoticMulBasisOfOrder {α : Type u_1} [CommMonoid α] (A : Set α) (n : ℕ) : Prop

A set A : Set α is an asymptotic multiplicative basis of order n if the elements that can be expressed as a product of n elements lying in A is cofinite.

Equations

• A.IsAsymptoticMulBasisOfOrder n = ∀ᶠ (a : α) in Filter.cofinite, a ∈ A ^ n

@[reducible, inline]

abbrev Set.IsAsymptoticAddBasisOfOrder {α : Type u_1} [AddCommMonoid α] (A : Set α) (n : ℕ) : Prop

A set A : Set α is an asymptotic additive basis of order n if the elements that can be expressed as a sum of n elements lying in A is cofinite.

Equations

• A.IsAsymptoticAddBasisOfOrder n = ∀ᶠ (a : α) in Filter.cofinite, a ∈ n • A

@[reducible, inline]

abbrev Set.IsAsymptoticMulBasis {α : Type u_1} [CommMonoid α] (A : Set α) : Prop

An asymptotic multiplicative basis of some order.

Equations

• A.IsAsymptoticMulBasis = ∃ (n : ℕ), A.IsAsymptoticMulBasisOfOrder n

@[reducible, inline]

abbrev Set.IsAsymptoticAddBasis {α : Type u_1} [AddCommMonoid α] (A : Set α) : Prop

An asymptotic additive basis of some order

Equations

• A.IsAsymptoticAddBasis = ∃ (n : ℕ), A.IsAsymptoticAddBasisOfOrder n

theorem Set.IsAsymptoticMulBasisOfOrder.toIsAsymptoticMulBasis {α : Type u_1} [CommMonoid α] {A : Set α} {n : ℕ} (hA : A.IsAsymptoticMulBasisOfOrder n) : A.IsAsymptoticMulBasis

theorem Set.IsAsymptoticAddBasisOfOrder.toIsAsymptoticAddBasis {α : Type u_1} [AddCommMonoid α] {A : Set α} {n : ℕ} (hA : A.IsAsymptoticAddBasisOfOrder n) : A.IsAsymptoticAddBasis

theorem Set.IsMulBasisOfOrder.toIsAsymptoticMulBasisOfOrder {α : Type u_1} [CommMonoid α] {A : Set α} {n : ℕ} (hA : A.IsMulBasisOfOrder n) : A.IsAsymptoticMulBasisOfOrder n

theorem Set.IsAddBasisOfOrder.toIsAsymptoticAddBasisOfOrder {α : Type u_1} [AddCommMonoid α] {A : Set α} {n : ℕ} (hA : A.IsAddBasisOfOrder n) : A.IsAsymptoticAddBasisOfOrder n

theorem Set.IsMulBasis.toIsAsymptoticMulBasis {α : Type u_1} [CommMonoid α] {A : Set α} (hA : A.IsMulBasis) : A.IsAsymptoticMulBasis

theorem Set.IsAddBasis.toIsAsymptoticAddBasis {α : Type u_1} [AddCommMonoid α] {A : Set α} (hA : A.IsAddBasis) : A.IsAsymptoticAddBasis

theorem Set.isAsymptoticMulBasisOfOrder_iff_prod {α : Type u_1} [CommMonoid α] (A : Set α) (n : ℕ) : A.IsAsymptoticMulBasisOfOrder n ↔ ∀ᶠ (a : α) in Filter.cofinite, ∃ (f : Fin n → α) (_ : ∀ (i : Fin n), f i ∈ A), ∏ i : Fin n, f i = a

A set A : Set α is an asymptotic multiplicative basis of order n if a cofinite set of a : α can be written as a = a₁ * ... * aₙ, where each aᵢ ∈ A.

theorem Set.isAsymptoticAddBasisOfOrder_iff_sum {α : Type u_1} [AddCommMonoid α] (A : Set α) (n : ℕ) : A.IsAsymptoticAddBasisOfOrder n ↔ ∀ᶠ (a : α) in Filter.cofinite, ∃ (f : Fin n → α) (_ : ∀ (i : Fin n), f i ∈ A), ∑ i : Fin n, f i = a

A set A : Set α is an asymptotic additive basis of order n if a cofinite set of a : α can be written as a = a₁ + ... + aₙ, where each aᵢ ∈ A.

theorem Set.isAsymptoticMulBasisOfOrder_two_iff {α : Type u_1} [CommMonoid α] (A : Set α) : A.IsAsymptoticMulBasisOfOrder 2 ↔ ∀ᶠ (a : α) in Filter.cofinite, a ∈ A * A

A set A : Set α is an asymptotic multiplicative basis of order 2 if a cofinite set of a : α belongs to A * A.

theorem Set.isAsymptoticAddBasisOfOrder_two_iff {α : Type u_1} [AddCommMonoid α] (A : Set α) : A.IsAsymptoticAddBasisOfOrder 2 ↔ ∀ᶠ (a : α) in Filter.cofinite, a ∈ A + A

A set A : Set α is an asymptotic additive basis of order 2 if a cofinite set of a : α belongs to A + A.

theorem Set.not_isAsymptoticMulBasisOfOrder_zero {α : Type u_1} [CommMonoid α] [Infinite α] (A : Set α) : ¬A.IsAsymptoticMulBasisOfOrder 0

If α is infinite, then no set A is an asymptotic multiplicative basis of order 0.

theorem Set.not_isAsymptoticAddBasisOfOrder_zero {α : Type u_1} [AddCommMonoid α] [Infinite α] (A : Set α) : ¬A.IsAsymptoticAddBasisOfOrder 0

If α is infinite, then no set A is an asymptotic additive basis of order 0.

theorem Set.isAsymptoticMulBasisOfOrder_one_iff {α : Type u_1} [CommMonoid α] (A : Set α) : A.IsAsymptoticMulBasisOfOrder 1 ↔ Aᶜ.Finite

A : Set α is an asymptotic basis of order one iff it is cofinite.

theorem Set.isAsymptoticAddBasisOfOrder_zero_iff {α : Type u_1} [AddCommMonoid α] (A : Set α) : A.IsAsymptoticAddBasisOfOrder 1 ↔ Aᶜ.Finite

A : Set α is an asymptotic basis of order one iff it is cofinite.

theorem Set.isAsymptoticMulBasisOfOrder_one_iff_Ioi {α : Type u_1} [CommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] (A : Set α) : A.IsAsymptoticMulBasisOfOrder 1 ↔ ∃ (a : α), Ioi a ⊆ A

For α equipped with a directed order, a set is an asymptotic multiplicative basis of order 1 if it contains an infinite tail of elements.

theorem Set.isAsymptoticAddBasisOfOrder_zero_iff_Ioi {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] (A : Set α) : A.IsAsymptoticAddBasisOfOrder 1 ↔ ∃ (a : α), Ioi a ⊆ A

A set is an asymptotic additive basis of order 1 if it contains an infinite tail of consecutive naturals.

theorem Set.isAsymptoticMulBasisOfOrder_one_iff_Ici {α : Type u_1} [CommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (A : Set α) : A.IsAsymptoticMulBasisOfOrder 1 ↔ ∃ (a : α), Ici a ⊆ A

For α equipped with a directed order, a set is an asymptotic multiplicative basis of order 1 if it contains an infinite tail of elements.

theorem Set.isAsymptoticAddBasisOfOrder_zero_iff_Ici {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (A : Set α) : A.IsAsymptoticAddBasisOfOrder 1 ↔ ∃ (a : α), Ici a ⊆ A

A set is an asymptotic additive basis of order 1 if it contains an infinite tail of consecutive naturals.

theorem Set.isAsymptoticMulBasisOfOrder_iff_atTop {α : Type u_1} [CommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (A : Set α) (n : ℕ) : A.IsAsymptoticMulBasisOfOrder n ↔ ∀ᶠ (a : α) in Filter.atTop, a ∈ A ^ n

theorem Set.isAsymptoticAddBasisOfOrder_iff_atTop {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (A : Set α) (n : ℕ) : A.IsAsymptoticAddBasisOfOrder n ↔ ∀ᶠ (a : α) in Filter.atTop, a ∈ n • A

theorem Set.isAsymptoticMulBasisOfOrder_iff_prod_atTop {α : Type u_1} [CommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (A : Set α) (n : ℕ) : A.IsAsymptoticMulBasisOfOrder n ↔ ∀ᶠ (a : α) in Filter.atTop, ∃ (f : Fin n → α) (_ : ∀ (i : Fin n), f i ∈ A), ∏ i : Fin n, f i = a

theorem Set.isAsymptoticAddBasisOfOrder_iff_sum_atTop {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (A : Set α) (n : ℕ) : A.IsAsymptoticAddBasisOfOrder n ↔ ∀ᶠ (a : α) in Filter.atTop, ∃ (f : Fin n → α) (_ : ∀ (i : Fin n), f i ∈ A), ∑ i : Fin n, f i = a