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

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

Equations

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

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

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

Equations

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

def Set.IsMulBasis {M : Type u_1} [CommMonoid M] (A : Set M) : Prop

A multiplicative basis of some order.

Equations

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

def Set.IsAddBasis {M : Type u_1} [AddCommMonoid M] (A : Set M) : Prop

An additive basis of some order.

Equations

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

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

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

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

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

@[simp]

theorem Set.not_isMulBasisOfOrder_zero {M : Type u_1} [CommMonoid M] {A : Set M} [Nontrivial M] : ¬A.IsMulBasisOfOrder 0

No set is a multiplicative basis of order 0.

@[simp]

theorem Set.not_isAddBasisOfOrder_zero {M : Type u_1} [AddCommMonoid M] {A : Set M} [Nontrivial M] : ¬A.IsAddBasisOfOrder 0

No set is an additive basis of order 0.

@[simp]

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

@[simp]

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

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

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

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

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

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

A set A : Set M 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 : M) in Filter.cofinite, a ∈ A ^ n

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

A set A : Set M 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 : M) in Filter.cofinite, a ∈ n • A

def Set.IsAsymptoticMulBasis {M : Type u_1} [CommMonoid M] (A : Set M) : Prop

An asymptotic multiplicative basis of some order.

Equations

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

def Set.IsAsymptoticAddBasis {M : Type u_1} [AddCommMonoid M] (A : Set M) : Prop

An asymptotic additive basis of some order.

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Set.IsAsymptoticMulBasisOfOrder.of_finite {M : Type u_1} [CommMonoid M] {A : Set M} {n : ℕ} [Finite M] : A.IsAsymptoticMulBasisOfOrder n

@[simp]

theorem Set.IsAsymptoticAddBasisOfOrder.of_finite {M : Type u_1} [AddCommMonoid M] {A : Set M} {n : ℕ} [Finite M] : A.IsAsymptoticAddBasisOfOrder n

@[simp]

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

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

@[simp]

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

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

theorem Set.IsAsymptoticMulBasisOfOrder.ne_zero {M : Type u_1} [CommMonoid M] {A : Set M} {n : ℕ} [Infinite M] (hA : A.IsAsymptoticMulBasisOfOrder n) : n ≠ 0

theorem Set.IsAsymptoticAddBasisOfOrder.ne_zero {M : Type u_1} [AddCommMonoid M] {A : Set M} {n : ℕ} [Infinite M] (hA : A.IsAsymptoticAddBasisOfOrder n) : n ≠ 0

theorem Set.IsAsymptoticMulBasisOfOrder.nonempty {M : Type u_1} [CommMonoid M] {A : Set M} {n : ℕ} [Infinite M] (hA : A.IsAsymptoticMulBasisOfOrder n) : A.Nonempty

theorem Set.IsAsymptoticAddBasisOfOrder.nonempty {M : Type u_1} [AddCommMonoid M] {A : Set M} {n : ℕ} [Infinite M] (hA : A.IsAsymptoticAddBasisOfOrder n) : A.Nonempty

@[simp]

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

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

@[simp]

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

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

theorem Set.IsAsymptoticMulBasisOfOrder.mono {M : Type u_1} [CommMonoid M] {A : Set M} {m n : ℕ} [LinearOrder M] [LocallyFiniteOrder M] [OrderBot M] [CanonicallyOrderedMul M] [IsCancelMul M] (hmn : m ≤ n) (hA : A.IsAsymptoticMulBasisOfOrder m) : A.IsAsymptoticMulBasisOfOrder n

theorem Set.IsAsymptoticAddBasisOfOrder.mono {M : Type u_1} [AddCommMonoid M] {A : Set M} {m n : ℕ} [LinearOrder M] [LocallyFiniteOrder M] [OrderBot M] [CanonicallyOrderedAdd M] [IsCancelAdd M] (hmn : m ≤ n) (hA : A.IsAsymptoticAddBasisOfOrder m) : A.IsAsymptoticAddBasisOfOrder n

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

For M 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 {M : Type u_1} [AddCommMonoid M] {A : Set M} [LinearOrder M] [LocallyFiniteOrder M] [OrderBot M] : A.IsAsymptoticAddBasisOfOrder 1 ↔ ∃ (a : M), Ioi a ⊆ A

For M equipped with a directed order, 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 {M : Type u_1} [CommMonoid M] {A : Set M} [LinearOrder M] [LocallyFiniteOrder M] [OrderBot M] [SuccOrder M] [NoMaxOrder M] : A.IsAsymptoticMulBasisOfOrder 1 ↔ ∃ (a : M), Ici a ⊆ A

For M 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 {M : Type u_1} [AddCommMonoid M] {A : Set M} [LinearOrder M] [LocallyFiniteOrder M] [OrderBot M] [SuccOrder M] [NoMaxOrder M] : A.IsAsymptoticAddBasisOfOrder 1 ↔ ∃ (a : M), Ici a ⊆ A

For M equipped with a directed order, a set is an asymptotic additive basis of order 1 if it contains an infinite tail of consecutive naturals.

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

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

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

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