Submonoids: membership criteria

In this file we prove various facts about membership in a submonoid:

• mem_iSup_of_directed, coe_iSup_of_directed, mem_sSup_of_directedOn, coe_sSup_of_directedOn: the supremum of a directed collection of submonoid is their union.
• sup_eq_range, mem_sup: supremum of two submonoids S, T of a commutative monoid is the set of products;
• closure_singleton_eq, mem_closure_singleton, mem_closure_pair: the multiplicative (resp., additive) closure of {x} consists of powers (resp., natural multiples) of x, and a similar result holds for the closure of {x, y}.

We also define Submonoid.powers and AddSubmonoid.multiples, the submonoids generated by a single element.

Tags

submonoid, submonoids

theorem Submonoid.mem_biSup_of_directedOn {M : Type u_1} [MulOneClass M] {ι : Type u_4} {p : ι → Prop} {K : ι → Submonoid M} {i : ι} (hp : p i) (hK : DirectedOn (Function.onFun (fun (x1 x2 : Submonoid M) => x1 ≤ x2) K) {i : ι | p i}) {x : M} : x ∈ ⨆ (i : ι), ⨆ (_ : p i), K i ↔ ∃ (i : ι), p i ∧ x ∈ K i

theorem AddSubmonoid.mem_biSup_of_directedOn {M : Type u_1} [AddZeroClass M] {ι : Type u_4} {p : ι → Prop} {K : ι → AddSubmonoid M} {i : ι} (hp : p i) (hK : DirectedOn (Function.onFun (fun (x1 x2 : AddSubmonoid M) => x1 ≤ x2) K) {i : ι | p i}) {x : M} : x ∈ ⨆ (i : ι), ⨆ (_ : p i), K i ↔ ∃ (i : ι), p i ∧ x ∈ K i

theorem Submonoid.mem_iSup_of_directed {M : Type u_1} [MulOneClass M] {ι : Sort u_4} [hι : Nonempty ι] {S : ι → Submonoid M} (hS : Directed (fun (x1 x2 : Submonoid M) => x1 ≤ x2) S) {x : M} : x ∈ ⨆ (i : ι), S i ↔ ∃ (i : ι), x ∈ S i

theorem AddSubmonoid.mem_iSup_of_directed {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} [hι : Nonempty ι] {S : ι → AddSubmonoid M} (hS : Directed (fun (x1 x2 : AddSubmonoid M) => x1 ≤ x2) S) {x : M} : x ∈ ⨆ (i : ι), S i ↔ ∃ (i : ι), x ∈ S i

@[simp]

theorem Submonoid.mem_iSup_prop {M : Type u_1} [MulOneClass M] {p : Prop} {S : p → Submonoid M} {x : M} : x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

@[simp]

theorem AddSubmonoid.mem_iSup_prop {M : Type u_1} [AddZeroClass M] {p : Prop} {S : p → AddSubmonoid M} {x : M} : x ∈ ⨆ (h : p), S h ↔ x = 0 ∨ ∃ (h : p), x ∈ S h

theorem Submonoid.coe_iSup_of_directed {M : Type u_1} [MulOneClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → Submonoid M} (hS : Directed (fun (x1 x2 : Submonoid M) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem AddSubmonoid.coe_iSup_of_directed {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → AddSubmonoid M} (hS : Directed (fun (x1 x2 : AddSubmonoid M) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem Submonoid.mem_sSup_of_directedOn {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : Submonoid M) => x1 ≤ x2) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

theorem AddSubmonoid.mem_sSup_of_directedOn {M : Type u_1} [AddZeroClass M] {S : Set (AddSubmonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : AddSubmonoid M) => x1 ≤ x2) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

theorem Submonoid.coe_sSup_of_directedOn {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : Submonoid M) => x1 ≤ x2) S) : ↑(sSup S) = ⋃ s ∈ S, ↑s

theorem AddSubmonoid.coe_sSup_of_directedOn {M : Type u_1} [AddZeroClass M] {S : Set (AddSubmonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : AddSubmonoid M) => x1 ≤ x2) S) : ↑(sSup S) = ⋃ s ∈ S, ↑s

theorem Submonoid.mem_sup_left {M : Type u_1} [MulOneClass M] {S T : Submonoid M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem AddSubmonoid.mem_sup_left {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem Submonoid.mem_sup_right {M : Type u_1} [MulOneClass M] {S T : Submonoid M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem AddSubmonoid.mem_sup_right {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem Submonoid.mul_mem_sup {M : Type u_1} [MulOneClass M] {S T : Submonoid M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem AddSubmonoid.add_mem_sup {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x + y ∈ S ⊔ T

theorem Submonoid.mem_iSup_of_mem {M : Type u_1} [MulOneClass M] {ι : Sort u_4} {S : ι → Submonoid M} (i : ι) {x : M} : x ∈ S i → x ∈ iSup S

theorem AddSubmonoid.mem_iSup_of_mem {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} {S : ι → AddSubmonoid M} (i : ι) {x : M} : x ∈ S i → x ∈ iSup S

theorem Submonoid.mem_sSup_of_mem {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} {s : Submonoid M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

theorem AddSubmonoid.mem_sSup_of_mem {M : Type u_1} [AddZeroClass M] {S : Set (AddSubmonoid M)} {s : AddSubmonoid M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

theorem Submonoid.iSup_induction {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), S i) (mem : ∀ (i : ι), ∀ x ∈ S i, motive x) (one : motive 1) (mul : ∀ (x y : M), motive x → motive y → motive (x * y)) : motive x

An induction principle for elements of ⨆ i, S i. If C holds for 1 and all elements of S i for all i, and is preserved under multiplication, then it holds for all elements of the supremum of S.

theorem AddSubmonoid.iSup_induction {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), S i) (mem : ∀ (i : ι), ∀ x ∈ S i, motive x) (zero : motive 0) (add : ∀ (x y : M), motive x → motive y → motive (x + y)) : motive x

An induction principle for elements of ⨆ i, S i. If C holds for 0 and all elements of S i for all i, and is preserved under addition, then it holds for all elements of the supremum of S.

theorem Submonoid.iSup_induction' {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {motive : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯) (one : motive 1 ⋯) (mul : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), motive x hx → motive y hy → motive (x * y) ⋯) {x : M} (hx : x ∈ ⨆ (i : ι), S i) : motive x hx

A dependent version of Submonoid.iSup_induction.

theorem AddSubmonoid.iSup_induction' {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M) {motive : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), motive x hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ ⨆ (i : ι), S i) : motive x hx

A dependent version of AddSubmonoid.iSup_induction.

theorem FreeMonoid.closure_range_of {α : Type u_4} : Submonoid.closure (Set.range of) = ⊤

theorem FreeAddMonoid.closure_range_of {α : Type u_4} : AddSubmonoid.closure (Set.range of) = ⊤

theorem Submonoid.closure_singleton_eq {M : Type u_1} [Monoid M] (x : M) : closure {x} = MonoidHom.mrange ((powersHom M) x)

theorem Submonoid.mem_closure_singleton {M : Type u_1} [Monoid M] {x y : M} : y ∈ closure {x} ↔ ∃ (n : ℕ), x ^ n = y

The submonoid generated by an element of a monoid equals the set of natural number powers of the element.

theorem Submonoid.mem_closure_singleton_self {M : Type u_1} [Monoid M] {y : M} : y ∈ closure {y}

theorem Submonoid.closure_singleton_one {M : Type u_1} [Monoid M] : closure {1} = ⊥

theorem Submonoid.card_bot {M : Type u_1} [Monoid M] {x✝ : Fintype ↥⊥} : Fintype.card ↥⊥ = 1

theorem AddSubmonoid.card_bot {M : Type u_1} [AddMonoid M] {x✝ : Fintype ↥⊥} : Fintype.card ↥⊥ = 1

theorem Submonoid.eq_bot_of_card_le {M : Type u_1} [Monoid M] {S : Submonoid M} [Fintype ↥S] (h : Fintype.card ↥S ≤ 1) : S = ⊥

theorem AddSubmonoid.eq_bot_of_card_le {M : Type u_1} [AddMonoid M] {S : AddSubmonoid M} [Fintype ↥S] (h : Fintype.card ↥S ≤ 1) : S = ⊥

theorem Submonoid.eq_bot_of_card_eq {M : Type u_1} [Monoid M] {S : Submonoid M} [Fintype ↥S] (h : Fintype.card ↥S = 1) : S = ⊥

theorem AddSubmonoid.eq_bot_of_card_eq {M : Type u_1} [AddMonoid M] {S : AddSubmonoid M} [Fintype ↥S] (h : Fintype.card ↥S = 1) : S = ⊥

theorem Submonoid.card_le_one_iff_eq_bot {M : Type u_1} [Monoid M] {S : Submonoid M} [Fintype ↥S] : Fintype.card ↥S ≤ 1 ↔ S = ⊥

theorem AddSubmonoid.card_le_one_iff_eq_bot {M : Type u_1} [AddMonoid M] {S : AddSubmonoid M} [Fintype ↥S] : Fintype.card ↥S ≤ 1 ↔ S = ⊥

theorem Submonoid.eq_bot_iff_card {M : Type u_1} [Monoid M] {S : Submonoid M} [Fintype ↥S] : S = ⊥ ↔ Fintype.card ↥S = 1

theorem AddSubmonoid.eq_bot_iff_card {M : Type u_1} [AddMonoid M] {S : AddSubmonoid M} [Fintype ↥S] : S = ⊥ ↔ Fintype.card ↥S = 1

theorem FreeMonoid.mrange_lift {M : Type u_1} [Monoid M] {α : Type u_4} (f : α → M) : MonoidHom.mrange (lift f) = Submonoid.closure (Set.range f)

theorem FreeAddMonoid.mrange_lift {M : Type u_1} [AddMonoid M] {α : Type u_4} (f : α → M) : AddMonoidHom.mrange (lift f) = AddSubmonoid.closure (Set.range f)

theorem Submonoid.closure_eq_mrange {M : Type u_1} [Monoid M] (s : Set M) : closure s = MonoidHom.mrange (FreeMonoid.lift Subtype.val)

theorem AddSubmonoid.closure_eq_mrange {M : Type u_1} [AddMonoid M] (s : Set M) : closure s = AddMonoidHom.mrange (FreeAddMonoid.lift Subtype.val)

theorem Submonoid.closure_eq_image_prod {M : Type u_1} [Monoid M] (s : Set M) : ↑(closure s) = List.prod '' {l : List M | ∀ x ∈ l, x ∈ s}

theorem AddSubmonoid.closure_eq_image_sum {M : Type u_1} [AddMonoid M] (s : Set M) : ↑(closure s) = List.sum '' {l : List M | ∀ x ∈ l, x ∈ s}

theorem Submonoid.exists_list_of_mem_closure {M : Type u_1} [Monoid M] {s : Set M} {x : M} (hx : x ∈ closure s) : ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x

theorem AddSubmonoid.exists_list_of_mem_closure {M : Type u_1} [AddMonoid M] {s : Set M} {x : M} (hx : x ∈ closure s) : ∃ (l : List M), (∀ y ∈ l, y ∈ s) ∧ l.sum = x

theorem Submonoid.exists_multiset_of_mem_closure {M : Type u_4} [CommMonoid M] {s : Set M} {x : M} (hx : x ∈ closure s) : ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.prod = x

theorem AddSubmonoid.exists_multiset_of_mem_closure {M : Type u_4} [AddCommMonoid M] {s : Set M} {x : M} (hx : x ∈ closure s) : ∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.sum = x

theorem Submonoid.closure_induction_left {M : Type u_1} [Monoid M] {s : Set M} {motive : (m : M) → m ∈ closure s → Prop} (one : motive 1 ⋯) (mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯) {x : M} (h : x ∈ closure s) : motive x h

theorem AddSubmonoid.closure_induction_left {M : Type u_1} [AddMonoid M] {s : Set M} {motive : (m : M) → m ∈ closure s → Prop} (zero : motive 0 ⋯) (add_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x + y) ⋯) {x : M} (h : x ∈ closure s) : motive x h

theorem Submonoid.induction_of_closure_eq_top_left {M : Type u_1} [Monoid M] {s : Set M} {motive : M → Prop} (hs : closure s = ⊤) (x : M) (one : motive 1) (mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)) : motive x

theorem AddSubmonoid.induction_of_closure_eq_top_left {M : Type u_1} [AddMonoid M] {s : Set M} {motive : M → Prop} (hs : closure s = ⊤) (x : M) (zero : motive 0) (add_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x + y)) : motive x

theorem Submonoid.closure_induction_right {M : Type u_1} [Monoid M] {s : Set M} {motive : (m : M) → m ∈ closure s → Prop} (one : motive 1 ⋯) (mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯) {x : M} (h : x ∈ closure s) : motive x h

theorem AddSubmonoid.closure_induction_right {M : Type u_1} [AddMonoid M] {s : Set M} {motive : (m : M) → m ∈ closure s → Prop} (zero : motive 0 ⋯) (add_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x + y) ⋯) {x : M} (h : x ∈ closure s) : motive x h

theorem Submonoid.induction_of_closure_eq_top_right {M : Type u_1} [Monoid M] {s : Set M} {motive : M → Prop} (hs : closure s = ⊤) (x : M) (one : motive 1) (mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)) : motive x

theorem AddSubmonoid.induction_of_closure_eq_top_right {M : Type u_1} [AddMonoid M] {s : Set M} {motive : M → Prop} (hs : closure s = ⊤) (x : M) (zero : motive 0) (add_right : ∀ (x y : M), y ∈ s → motive x → motive (x + y)) : motive x

def Submonoid.powers {M : Type u_1} [Monoid M] (n : M) : Submonoid M

The submonoid generated by an element.

@[simp]

theorem Submonoid.mem_powers {M : Type u_1} [Monoid M] (n : M) : n ∈ powers n

theorem Submonoid.coe_powers {M : Type u_1} [Monoid M] (x : M) : ↑(powers x) = Set.range fun (n : ℕ) => x ^ n

theorem Submonoid.mem_powers_iff {M : Type u_1} [Monoid M] (x z : M) : x ∈ powers z ↔ ∃ (n : ℕ), z ^ n = x

@[implicit_reducible]

noncomputable instance Submonoid.decidableMemPowers {M : Type u_1} [Monoid M] {a : M} : DecidablePred fun (x : M) => x ∈ powers a

@[implicit_reducible]

noncomputable instance Submonoid.fintypePowers {M : Type u_1} [Monoid M] {a : M} [Fintype M] : Fintype ↥(powers a)

theorem Submonoid.powers_eq_closure {M : Type u_1} [Monoid M] (n : M) : powers n = closure {n}

theorem Submonoid.powers_le {M : Type u_1} [Monoid M] {n : M} {P : Submonoid M} : powers n ≤ P ↔ n ∈ P

@[simp]

theorem Submonoid.powers_one {M : Type u_1} [Monoid M] : powers 1 = ⊥

theorem IsIdempotentElem.coe_powers {M : Type u_1} [Monoid M] {a : M} (ha : IsIdempotentElem a) : ↑(Submonoid.powers a) = {1, a}

@[reducible, inline]

abbrev Submonoid.groupPowers {M : Type u_1} [Monoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group ↥(powers x)

The submonoid generated by an element is a group if that element has finite order.

def Submonoid.pow {M : Type u_1} [Monoid M] (n : M) (m : ℕ) : ↥(powers n)

Exponentiation map from natural numbers to powers.

@[simp]

theorem Submonoid.pow_coe {M : Type u_1} [Monoid M] (n : M) (m : ℕ) : ↑(pow n m) = n ^ m

theorem Submonoid.pow_apply {M : Type u_1} [Monoid M] (n : M) (m : ℕ) : pow n m = ⟨n ^ m, ⋯⟩

def Submonoid.log {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (p : ↥(powers n)) : ℕ

Logarithms from powers to natural numbers.

@[simp]

theorem Submonoid.pow_log_eq_self {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (p : ↥(powers n)) : pow n (log p) = p

theorem Submonoid.pow_right_injective_iff_pow_injective {M : Type u_1} [Monoid M] {n : M} : (Function.Injective fun (m : ℕ) => n ^ m) ↔ Function.Injective (pow n)

@[simp]

theorem Submonoid.log_pow_eq_self {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ℕ) => n ^ m) (m : ℕ) : log (pow n m) = m

def Submonoid.powLogEquiv {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ℕ) => n ^ m) : Multiplicative ℕ ≃* ↥(powers n)

The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers when it is injective. The inverse is given by the logarithms.

@[simp]

theorem Submonoid.powLogEquiv_symm_apply {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ℕ) => n ^ m) (m : ↥(powers n)) : (powLogEquiv h).symm m = Multiplicative.ofAdd (log m)

@[simp]

theorem Submonoid.powLogEquiv_apply {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ℕ) => n ^ m) (m : Multiplicative ℕ) : (powLogEquiv h) m = pow n (Multiplicative.toAdd m)

theorem Submonoid.log_mul {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ℕ) => n ^ m) (x y : ↥(powers n)) : log (x * y) = log x + log y

theorem Submonoid.log_pow_int_eq_self {x : ℤ} (h : 1 < x.natAbs) (m : ℕ) : log (pow x m) = m

@[simp]

theorem Submonoid.map_powers {M : Type u_1} [Monoid M] {N : Type u_4} {F : Type u_5} [Monoid N] [FunLike F M N] [MonoidHomClass F M N] (f : F) (m : M) : map f (powers m) = powers (f m)

theorem IsScalarTower.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [Monoid M] [MulAction M N] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤) (hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z) : IsScalarTower M N α

theorem VAddAssocClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [AddMonoid M] [AddAction M N] [VAdd N α] [AddAction M α] {s : Set M} (htop : AddSubmonoid.closure s = ⊤) (hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x +ᵥ y) +ᵥ z = x +ᵥ y +ᵥ z) : VAddAssocClass M N α

theorem SMulCommClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [Monoid M] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤) (hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z) : SMulCommClass M N α

theorem VAddCommClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [AddMonoid M] [VAdd N α] [AddAction M α] {s : Set M} (htop : AddSubmonoid.closure s = ⊤) (hs : ∀ x ∈ s, ∀ (y : N) (z : α), x +ᵥ y +ᵥ z = y +ᵥ x +ᵥ z) : VAddCommClass M N α

theorem Submonoid.sup_eq_range {N : Type u_4} [CommMonoid N] (s t : Submonoid N) : s ⊔ t = MonoidHom.mrange (s.subtype.coprod t.subtype)

theorem AddSubmonoid.sup_eq_range {N : Type u_4} [AddCommMonoid N] (s t : AddSubmonoid N) : s ⊔ t = AddMonoidHom.mrange (s.subtype.coprod t.subtype)

theorem Submonoid.mem_sup {N : Type u_4} [CommMonoid N] {s t : Submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

theorem AddSubmonoid.mem_sup {N : Type u_4} [AddCommMonoid N] {s t : AddSubmonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x

@[simp]

theorem Submonoid.forall_mem_sup {N : Type u_4} [CommMonoid N] {P : N → Prop} {s t : Submonoid N} : (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

theorem AddSubmonoid.forall_mem_sup {N : Type u_4} [AddCommMonoid N] {P : N → Prop} {s t : AddSubmonoid N} : (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ + x₂)

@[simp]

theorem Submonoid.exists_mem_sup {N : Type u_4} [CommMonoid N] {P : N → Prop} {s t : Submonoid N} : (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

theorem AddSubmonoid.exists_mem_sup {N : Type u_4} [AddCommMonoid N] {P : N → Prop} {s t : AddSubmonoid N} : (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ + x₂)

theorem AddSubmonoid.closure_singleton_eq {A : Type u_2} [AddMonoid A] (x : A) : closure {x} = AddMonoidHom.mrange ((multiplesHom A) x)

theorem AddSubmonoid.mem_closure_singleton {A : Type u_2} [AddMonoid A] {x y : A} : y ∈ closure {x} ↔ ∃ (n : ℕ), n • x = y

The AddSubmonoid generated by an element of an AddMonoid equals the set of natural number multiples of the element.

theorem AddSubmonoid.closure_singleton_zero {A : Type u_2} [AddMonoid A] : closure {0} = ⊥

def AddSubmonoid.multiples {A : Type u_2} [AddMonoid A] (x : A) : AddSubmonoid A

The additive submonoid generated by an element.

@[simp]

theorem AddSubmonoid.mem_multiples {M : Type u_1} [AddMonoid M] (n : M) : n ∈ multiples n

theorem AddSubmonoid.coe_multiples {M : Type u_1} [AddMonoid M] (x : M) : ↑(multiples x) = Set.range fun (n : ℕ) => n • x

theorem AddSubmonoid.mem_multiples_iff {M : Type u_1} [AddMonoid M] (x z : M) : x ∈ multiples z ↔ ∃ (n : ℕ), n • z = x

@[implicit_reducible]

noncomputable instance AddSubmonoid.decidableMemMultiples {M : Type u_1} [AddMonoid M] {a : M} : DecidablePred fun (x : M) => x ∈ multiples a

@[implicit_reducible]

noncomputable instance AddSubmonoid.fintypeMultiples {M : Type u_1} [AddMonoid M] {a : M} [Fintype M] : Fintype ↥(multiples a)

theorem AddSubmonoid.multiples_eq_closure {M : Type u_1} [AddMonoid M] (n : M) : multiples n = closure {n}

theorem AddSubmonoid.multiples_le {M : Type u_1} [AddMonoid M] {n : M} {P : AddSubmonoid M} : multiples n ≤ P ↔ n ∈ P

@[simp]

theorem AddSubmonoid.multiples_zero {M : Type u_1} [AddMonoid M] : multiples 0 = ⊥

@[reducible, inline]

abbrev AddSubmonoid.addGroupMultiples {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : n • x = 0) : AddGroup ↥(multiples x)

The additive submonoid generated by an element is an additive group if that element has finite order.

theorem Submonoid.mem_closure_pair {A : Type u_4} [CommMonoid A] (a b c : A) : c ∈ closure {a, b} ↔ ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c

An element is in the closure of a two-element set if it is a linear combination of those two elements.

theorem AddSubmonoid.mem_closure_pair {A : Type u_4} [AddCommMonoid A] (a b c : A) : c ∈ closure {a, b} ↔ ∃ (m : ℕ) (n : ℕ), m • a + n • b = c

An element is in the closure of a two-element set if it is a linear combination of those two elements.

theorem ofMul_image_powers_eq_multiples_ofMul {M : Type u_1} [Monoid M] {x : M} : ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))

theorem ofAdd_image_multiples_eq_powers_ofAdd {A : Type u_2} [AddMonoid A] {x : A} : ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))

@[simp]

theorem Nat.addSubmonoidClosure_one : AddSubmonoid.closure {1} = ⊤