Documentation

Mathlib.GroupTheory.Submonoid.Membership

Submonoids: membership criteria #

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

Tags #

submonoid, submonoids

@[simp]
theorem AddSubmonoidClass.coe_list_sum {M : Type u_1} {B : Type u_2} [inst : AddMonoid M] [inst : SetLike B M] [inst : AddSubmonoidClass B M] {S : B} (l : List { x // x S }) :
↑(List.sum l) = List.sum (List.map Subtype.val l)
@[simp]
theorem SubmonoidClass.coe_list_prod {M : Type u_1} {B : Type u_2} [inst : Monoid M] [inst : SetLike B M] [inst : SubmonoidClass B M] {S : B} (l : List { x // x S }) :
↑(List.prod l) = List.prod (List.map Subtype.val l)
@[simp]
theorem AddSubmonoidClass.coe_multiset_sum {B : Type u_2} {S : B} {M : Type u_1} [inst : AddCommMonoid M] [inst : SetLike B M] [inst : AddSubmonoidClass B M] (m : Multiset { x // x S }) :
↑(Multiset.sum m) = Multiset.sum (Multiset.map Subtype.val m)
@[simp]
theorem SubmonoidClass.coe_multiset_prod {B : Type u_2} {S : B} {M : Type u_1} [inst : CommMonoid M] [inst : SetLike B M] [inst : SubmonoidClass B M] (m : Multiset { x // x S }) :
↑(Multiset.prod m) = Multiset.prod (Multiset.map Subtype.val m)
theorem AddSubmonoidClass.coe_finset_sum {B : Type u_3} {S : B} {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst : SetLike B M] [inst : AddSubmonoidClass B M] (f : ι{ x // x S }) (s : Finset ι) :
↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)
theorem SubmonoidClass.coe_finset_prod {B : Type u_3} {S : B} {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst : SetLike B M] [inst : SubmonoidClass B M] (f : ι{ x // x S }) (s : Finset ι) :
↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)
theorem list_sum_mem {M : Type u_1} {B : Type u_2} [inst : AddMonoid M] [inst : SetLike B M] [inst : AddSubmonoidClass B M] {S : B} {l : List M} (hl : ∀ (x : M), x lx S) :

Sum of a list of elements in an AddSubmonoid is in the AddSubmonoid.

theorem list_prod_mem {M : Type u_1} {B : Type u_2} [inst : Monoid M] [inst : SetLike B M] [inst : SubmonoidClass B M] {S : B} {l : List M} (hl : ∀ (x : M), x lx S) :

Product of a list of elements in a submonoid is in the submonoid.

theorem multiset_sum_mem {B : Type u_2} {S : B} {M : Type u_1} [inst : AddCommMonoid M] [inst : SetLike B M] [inst : AddSubmonoidClass B M] (m : Multiset M) (hm : ∀ (a : M), a ma S) :

Sum of a multiset of elements in an AddSubmonoid of an AddCommMonoid is in the AddSubmonoid.

theorem multiset_prod_mem {B : Type u_2} {S : B} {M : Type u_1} [inst : CommMonoid M] [inst : SetLike B M] [inst : SubmonoidClass B M] (m : Multiset M) (hm : ∀ (a : M), a ma S) :

Product of a multiset of elements in a submonoid of a CommMonoid is in the submonoid.

abbrev sum_mem.match_1 {M : Type u_2} {ι : Type u_1} {t : Finset ι} {f : ιM} (_x : M) (motive : (a, a t.val f a = _x) → Prop) :
(x : a, a t.val f a = _x) → ((i : ι) → (hi : i t.val) → (hix : f i = _x) → motive (_ : a, a t.val f a = _x)) → motive x
Equations
theorem sum_mem {B : Type u_2} {S : B} {M : Type u_1} [inst : AddCommMonoid M] [inst : SetLike B M] [inst : AddSubmonoidClass B M] {ι : Type u_3} {t : Finset ι} {f : ιM} (h : ∀ (c : ι), c tf c S) :
(Finset.sum t fun c => f c) S

Sum of elements in an AddSubmonoid of an AddCommMonoid indexed by a Finset is in the AddSubmonoid.

theorem prod_mem {B : Type u_2} {S : B} {M : Type u_1} [inst : CommMonoid M] [inst : SetLike B M] [inst : SubmonoidClass B M] {ι : Type u_3} {t : Finset ι} {f : ιM} (h : ∀ (c : ι), c tf c S) :
(Finset.prod t fun c => f c) S

Product of elements of a submonoid of a CommMonoid indexed by a Finset is in the submonoid.

theorem AddSubmonoid.coe_list_sum {M : Type u_1} [inst : AddMonoid M] (s : AddSubmonoid M) (l : List { x // x s }) :
↑(List.sum l) = List.sum (List.map Subtype.val l)
theorem Submonoid.coe_list_prod {M : Type u_1} [inst : Monoid M] (s : Submonoid M) (l : List { x // x s }) :
↑(List.prod l) = List.prod (List.map Subtype.val l)
theorem AddSubmonoid.coe_multiset_sum {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset { x // x S }) :
↑(Multiset.sum m) = Multiset.sum (Multiset.map Subtype.val m)
theorem Submonoid.coe_multiset_prod {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (m : Multiset { x // x S }) :
↑(Multiset.prod m) = Multiset.prod (Multiset.map Subtype.val m)
@[simp]
theorem AddSubmonoid.coe_finset_sum {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (S : AddSubmonoid M) (f : ι{ x // x S }) (s : Finset ι) :
↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)
@[simp]
theorem Submonoid.coe_finset_prod {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (S : Submonoid M) (f : ι{ x // x S }) (s : Finset ι) :
↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)
theorem AddSubmonoid.list_sum_mem {M : Type u_1} [inst : AddMonoid M] (s : AddSubmonoid M) {l : List M} (hl : ∀ (x : M), x lx s) :

Sum of a list of elements in an AddSubmonoid is in the AddSubmonoid.

theorem Submonoid.list_prod_mem {M : Type u_1} [inst : Monoid M] (s : Submonoid M) {l : List M} (hl : ∀ (x : M), x lx s) :

Product of a list of elements in a submonoid is in the submonoid.

theorem AddSubmonoid.multiset_sum_mem {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M) (hm : ∀ (a : M), a ma S) :

Sum of a multiset of elements in an AddSubmonoid of an AddCommMonoid is in the AddSubmonoid.

theorem Submonoid.multiset_prod_mem {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (m : Multiset M) (hm : ∀ (a : M), a ma S) :

Product of a multiset of elements in a submonoid of a CommMonoid is in the submonoid.

theorem AddSubmonoid.multiset_noncommSum_mem {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (m : Multiset M) (comm : Set.Pairwise { x | x m } AddCommute) (h : ∀ (x : M), x mx S) :
theorem Submonoid.multiset_noncommProd_mem {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (m : Multiset M) (comm : Set.Pairwise { x | x m } Commute) (h : ∀ (x : M), x mx S) :
theorem AddSubmonoid.sum_mem {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) {ι : Type u_2} {t : Finset ι} {f : ιM} (h : ∀ (c : ι), c tf c S) :
(Finset.sum t fun c => f c) S

Sum of elements in an AddSubmonoid of an AddCommMonoid indexed by a Finset is in the AddSubmonoid.

theorem Submonoid.prod_mem {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) {ι : Type u_2} {t : Finset ι} {f : ιM} (h : ∀ (c : ι), c tf c S) :
(Finset.prod t fun c => f c) S

Product of elements of a submonoid of a CommMonoid indexed by a Finset is in the submonoid.

theorem AddSubmonoid.noncommSum_mem {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {ι : Type u_2} (t : Finset ι) (f : ιM) (comm : Set.Pairwise t fun a b => AddCommute (f a) (f b)) (h : ∀ (c : ι), c tf c S) :
theorem Submonoid.noncommProd_mem {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {ι : Type u_2} (t : Finset ι) (f : ιM) (comm : Set.Pairwise t fun a b => Commute (f a) (f b)) (h : ∀ (c : ι), c tf c S) :
abbrev AddSubmonoid.mem_supᵢ_of_directed.match_1 {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} {S : ιAddSubmonoid M} {x : M} (motive : (i, x S i) → Prop) :
(x : i, x S i) → ((i : ι) → (hi : x S i) → motive (_ : i, x S i)) → motive x
Equations
theorem AddSubmonoid.mem_supᵢ_of_directed {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} [hι : Nonempty ι] {S : ιAddSubmonoid M} (hS : Directed (fun x x_1 => x x_1) S) {x : M} :
(x i, S i) i, x S i
theorem Submonoid.mem_supᵢ_of_directed {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} [hι : Nonempty ι] {S : ιSubmonoid M} (hS : Directed (fun x x_1 => x x_1) S) {x : M} :
(x i, S i) i, x S i
theorem AddSubmonoid.coe_supᵢ_of_directed {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} [inst : Nonempty ι] {S : ιAddSubmonoid M} (hS : Directed (fun x x_1 => x x_1) S) :
↑(i, S i) = Set.unionᵢ fun i => ↑(S i)
theorem Submonoid.coe_supᵢ_of_directed {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} [inst : Nonempty ι] {S : ιSubmonoid M} (hS : Directed (fun x x_1 => x x_1) S) :
↑(i, S i) = Set.unionᵢ fun i => ↑(S i)
theorem AddSubmonoid.mem_supₛ_of_directedOn {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) {x : M} :
x supₛ S s, s S x s
theorem Submonoid.mem_supₛ_of_directedOn {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) {x : M} :
x supₛ S s, s S x s
theorem AddSubmonoid.coe_supₛ_of_directedOn {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) :
↑(supₛ S) = Set.unionᵢ fun s => Set.unionᵢ fun h => s
theorem Submonoid.coe_supₛ_of_directedOn {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) :
↑(supₛ S) = Set.unionᵢ fun s => Set.unionᵢ fun h => s
theorem AddSubmonoid.mem_sup_left {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} :
x Sx S T
theorem Submonoid.mem_sup_left {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} :
x Sx S T
theorem AddSubmonoid.mem_sup_right {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} :
x Tx S T
theorem Submonoid.mem_sup_right {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} :
x Tx S T
theorem AddSubmonoid.add_mem_sup {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} {y : M} (hx : x S) (hy : y T) :
x + y S T
theorem Submonoid.mul_mem_sup {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} {y : M} (hx : x S) (hy : y T) :
x * y S T
theorem AddSubmonoid.mem_supᵢ_of_mem {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} {S : ιAddSubmonoid M} (i : ι) {x : M} :
x S ix supᵢ S
theorem Submonoid.mem_supᵢ_of_mem {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} {S : ιSubmonoid M} (i : ι) {x : M} :
x S ix supᵢ S
theorem AddSubmonoid.mem_supₛ_of_mem {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)} {s : AddSubmonoid M} (hs : s S) {x : M} :
x sx supₛ S
theorem Submonoid.mem_supₛ_of_mem {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)} {s : Submonoid M} (hs : s S) {x : M} :
x sx supₛ S
theorem AddSubmonoid.supᵢ_induction {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} (S : ιAddSubmonoid M) {C : MProp} {x : M} (hx : x i, S i) (hp : (i : ι) → (x : M) → x S iC x) (h1 : C 0) (hmul : (x y : M) → C xC yC (x + y)) :
C 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.supᵢ_induction {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} (S : ιSubmonoid M) {C : MProp} {x : M} (hx : x i, S i) (hp : (i : ι) → (x : M) → x S iC x) (h1 : C 1) (hmul : (x y : M) → C xC yC (x * y)) :
C 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.supᵢ_induction' {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} (S : ιAddSubmonoid M) {C : (x : M) → (x i, S i) → Prop} (hp : (i : ι) → (x : M) → (hxS : x S i) → C x (_ : x i, S i)) (h1 : C 0 (_ : 0 i, S i)) (hmul : (x y : M) → (hx : x i, S i) → (hy : y i, S i) → C x hxC y hyC (x + y) (_ : x + y i, S i)) {x : M} (hx : x i, S i) :
C x hx

A dependent version of AddSubmonoid.supᵢ_induction.

theorem Submonoid.supᵢ_induction' {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} (S : ιSubmonoid M) {C : (x : M) → (x i, S i) → Prop} (hp : (i : ι) → (x : M) → (hxS : x S i) → C x (_ : x i, S i)) (h1 : C 1 (_ : 1 i, S i)) (hmul : (x y : M) → (hx : x i, S i) → (hy : y i, S i) → C x hxC y hyC (x * y) (_ : x * y i, S i)) {x : M} (hx : x i, S i) :
C x hx

A dependent version of Submonoid.supᵢ_induction.

theorem Submonoid.mem_closure_singleton {M : Type u_1} [inst : Monoid M] {x : M} {y : M} :
y Submonoid.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 FreeAddMonoid.mrange_lift {M : Type u_2} [inst : AddMonoid M] {α : Type u_1} (f : αM) :
AddMonoidHom.mrange (FreeAddMonoid.lift f) = AddSubmonoid.closure (Set.range f)
theorem FreeMonoid.mrange_lift {M : Type u_2} [inst : Monoid M] {α : Type u_1} (f : αM) :
MonoidHom.mrange (FreeMonoid.lift f) = Submonoid.closure (Set.range f)
theorem AddSubmonoid.closure_eq_mrange {M : Type u_1} [inst : AddMonoid M] (s : Set M) :
AddSubmonoid.closure s = AddMonoidHom.mrange (FreeAddMonoid.lift Subtype.val)
theorem Submonoid.closure_eq_mrange {M : Type u_1} [inst : Monoid M] (s : Set M) :
Submonoid.closure s = MonoidHom.mrange (FreeMonoid.lift Subtype.val)
theorem AddSubmonoid.closure_eq_image_sum {M : Type u_1} [inst : AddMonoid M] (s : Set M) :
↑(AddSubmonoid.closure s) = List.sum '' { l | ∀ (x : M), x lx s }
theorem Submonoid.closure_eq_image_prod {M : Type u_1} [inst : Monoid M] (s : Set M) :
↑(Submonoid.closure s) = List.prod '' { l | ∀ (x : M), x lx s }
theorem AddSubmonoid.exists_list_of_mem_closure {M : Type u_1} [inst : AddMonoid M] {s : Set M} {x : M} (hx : x AddSubmonoid.closure s) :
l x, List.sum l = x
theorem Submonoid.exists_list_of_mem_closure {M : Type u_1} [inst : Monoid M] {s : Set M} {x : M} (hx : x Submonoid.closure s) :
l x, List.prod l = x
theorem AddSubmonoid.exists_multiset_of_mem_closure {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} {x : M} (hx : x AddSubmonoid.closure s) :
l x, Multiset.sum l = x
theorem Submonoid.exists_multiset_of_mem_closure {M : Type u_1} [inst : CommMonoid M] {s : Set M} {x : M} (hx : x Submonoid.closure s) :
l x, Multiset.prod l = x
theorem AddSubmonoid.closure_induction_left {M : Type u_1} [inst : AddMonoid M] {s : Set M} {p : MProp} {x : M} (h : x AddSubmonoid.closure s) (H1 : p 0) (Hmul : (x : M) → x s(y : M) → p yp (x + y)) :
p x
theorem Submonoid.closure_induction_left {M : Type u_1} [inst : Monoid M] {s : Set M} {p : MProp} {x : M} (h : x Submonoid.closure s) (H1 : p 1) (Hmul : (x : M) → x s(y : M) → p yp (x * y)) :
p x
theorem AddSubmonoid.induction_of_closure_eq_top_left {M : Type u_1} [inst : AddMonoid M] {s : Set M} {p : MProp} (hs : AddSubmonoid.closure s = ) (x : M) (H1 : p 0) (Hmul : (x : M) → x s(y : M) → p yp (x + y)) :
p x
theorem Submonoid.induction_of_closure_eq_top_left {M : Type u_1} [inst : Monoid M] {s : Set M} {p : MProp} (hs : Submonoid.closure s = ) (x : M) (H1 : p 1) (Hmul : (x : M) → x s(y : M) → p yp (x * y)) :
p x
theorem AddSubmonoid.closure_induction_right {M : Type u_1} [inst : AddMonoid M] {s : Set M} {p : MProp} {x : M} (h : x AddSubmonoid.closure s) (H1 : p 0) (Hmul : (x y : M) → y sp xp (x + y)) :
p x
theorem Submonoid.closure_induction_right {M : Type u_1} [inst : Monoid M] {s : Set M} {p : MProp} {x : M} (h : x Submonoid.closure s) (H1 : p 1) (Hmul : (x y : M) → y sp xp (x * y)) :
p x
theorem AddSubmonoid.induction_of_closure_eq_top_right {M : Type u_1} [inst : AddMonoid M] {s : Set M} {p : MProp} (hs : AddSubmonoid.closure s = ) (x : M) (H1 : p 0) (Hmul : (x y : M) → y sp xp (x + y)) :
p x
theorem Submonoid.induction_of_closure_eq_top_right {M : Type u_1} [inst : Monoid M] {s : Set M} {p : MProp} (hs : Submonoid.closure s = ) (x : M) (H1 : p 1) (Hmul : (x y : M) → y sp xp (x * y)) :
p x
def Submonoid.powers {M : Type u_1} [inst : Monoid M] (n : M) :

The submonoid generated by an element.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Submonoid.mem_powers {M : Type u_1} [inst : Monoid M] (n : M) :
theorem Submonoid.mem_powers_iff {M : Type u_1} [inst : Monoid M] (x : M) (z : M) :
x Submonoid.powers z n, z ^ n = x
theorem Submonoid.powers_subset {M : Type u_1} [inst : Monoid M] {n : M} {P : Submonoid M} (h : n P) :
@[simp]
theorem Submonoid.powers_one {M : Type u_1} [inst : Monoid M] :
@[simp]
theorem Submonoid.pow_coe {M : Type u_1} [inst : Monoid M] (n : M) (m : ) :
↑(Submonoid.pow n m) = n ^ m
def Submonoid.pow {M : Type u_1} [inst : Monoid M] (n : M) (m : ) :
{ x // x Submonoid.powers n }

Exponentiation map from natural numbers to powers.

Equations
theorem Submonoid.pow_apply {M : Type u_1} [inst : Monoid M] (n : M) (m : ) :
Submonoid.pow n m = { val := n ^ m, property := (_ : y, (fun x x_1 => x ^ x_1) n y = n ^ m) }
def Submonoid.log {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (p : { x // x Submonoid.powers n }) :

Logarithms from powers to natural numbers.

Equations
@[simp]
theorem Submonoid.pow_log_eq_self {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (p : { x // x Submonoid.powers n }) :
@[simp]
theorem Submonoid.log_pow_eq_self {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (m : ) :
@[simp]
theorem Submonoid.powLogEquiv_apply {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (m : Multiplicative ) :
↑(Submonoid.powLogEquiv h) m = Submonoid.pow n (Multiplicative.toAdd m)
@[simp]
theorem Submonoid.powLogEquiv_symm_apply {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (m : { x // x Submonoid.powers n }) :
↑(MulEquiv.symm (Submonoid.powLogEquiv h)) m = Multiplicative.ofAdd (Submonoid.log m)
def Submonoid.powLogEquiv {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) :

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.

Equations
  • One or more equations did not get rendered due to their size.
theorem Submonoid.log_mul {M : Type u_1} [inst : Monoid M] [inst : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (x : { x // x Submonoid.powers n }) (y : { x // x Submonoid.powers n }) :
@[simp]
theorem Submonoid.map_powers {M : Type u_3} [inst : Monoid M] {N : Type u_1} {F : Type u_2} [inst : Monoid N] [inst : MonoidHomClass F M N] (f : F) (m : M) :
def AddSubmonoid.closureAddCommMonoidOfComm {M : Type u_1} [inst : AddMonoid M] {s : Set M} (hcomm : ∀ (a : M), a s∀ (b : M), b sa + b = b + a) :

If all the elements of a set s commute, then closure s forms an additive commutative monoid.

Equations
def AddSubmonoid.closureAddCommMonoidOfComm.proof_5 {M : Type u_1} [inst : AddMonoid M] {s : Set M} (hcomm : ∀ (a : M), a s∀ (b : M), b sa + b = b + a) (x : { x // x AddSubmonoid.closure s }) (y : { x // x AddSubmonoid.closure s }) :
x + y = y + x
Equations
  • (_ : x + y = y + x) = (_ : x + y = y + x)
def AddSubmonoid.closureAddCommMonoidOfComm.proof_4 {M : Type u_1} [inst : AddMonoid M] {s : Set M} (n : ) (x : { x // x AddSubmonoid.closure s }) :
Equations
  • One or more equations did not get rendered due to their size.
def AddSubmonoid.closureAddCommMonoidOfComm.proof_1 {M : Type u_1} [inst : AddMonoid M] {s : Set M} (a : { x // x AddSubmonoid.closure s }) :
0 + a = a
Equations
Equations
def AddSubmonoid.closureAddCommMonoidOfComm.proof_2 {M : Type u_1} [inst : AddMonoid M] {s : Set M} (a : { x // x AddSubmonoid.closure s }) :
a + 0 = a
Equations
def Submonoid.closureCommMonoidOfComm {M : Type u_1} [inst : Monoid M] {s : Set M} (hcomm : ∀ (a : M), a s∀ (b : M), b sa * b = b * a) :

If all the elements of a set s commute, then closure s is a commutative monoid.

Equations
theorem VAddAssocClass.of_mclosure_eq_top {M : Type u_3} {N : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M N] [inst : VAdd N α] [inst : AddAction M α] {s : Set M} (htop : AddSubmonoid.closure s = ) (hs : ∀ (x : M), x s∀ (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)) :
theorem IsScalarTower.of_mclosure_eq_top {M : Type u_3} {N : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : MulAction M N] [inst : SMul N α] [inst : MulAction M α] {s : Set M} (htop : Submonoid.closure s = ) (hs : ∀ (x : M), x s∀ (y : N) (z : α), (x y) z = x y z) :
theorem VAddCommClass.of_mclosure_eq_top {M : Type u_3} {N : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd N α] [inst : AddAction M α] {s : Set M} (htop : AddSubmonoid.closure s = ) (hs : ∀ (x : M), x s∀ (y : N) (z : α), x +ᵥ (y +ᵥ z) = y +ᵥ (x +ᵥ z)) :
theorem SMulCommClass.of_mclosure_eq_top {M : Type u_3} {N : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul N α] [inst : MulAction M α] {s : Set M} (htop : Submonoid.closure s = ) (hs : ∀ (x : M), x s∀ (y : N) (z : α), x y z = y x z) :
theorem AddSubmonoid.mem_sup {N : Type u_1} [inst : AddCommMonoid N] {s : AddSubmonoid N} {t : AddSubmonoid N} {x : N} :
x s t y, y s z, z t y + z = x
theorem Submonoid.mem_sup {N : Type u_1} [inst : CommMonoid N] {s : Submonoid N} {t : Submonoid N} {x : N} :
x s t y, y s z, z t y * z = x
theorem AddSubmonoid.mem_closure_singleton {A : Type u_1} [inst : AddMonoid A] {x : A} {y : A} :
y AddSubmonoid.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.

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

The additive submonoid generated by an element.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubmonoid.mem_multiples {M : Type u_1} [inst : AddMonoid M] (n : M) :
theorem AddSubmonoid.mem_multiples_iff {M : Type u_1} [inst : AddMonoid M] (x : M) (z : M) :
theorem AddSubmonoid.multiples_subset {M : Type u_1} [inst : AddMonoid M] {n : M} {P : AddSubmonoid M} (h : n P) :
abbrev AddSubmonoid.multiples_subset.match_1 {M : Type u_1} [inst : AddMonoid M] {n : M} (motive : (x : M) → x AddSubmonoid.multiples nProp) :
(x : M) → (hx : x AddSubmonoid.multiples n) → ((i : ) → motive ((fun x x_1 => x_1 x) n i) (_ : y, (fun x x_1 => x_1 x) n y = (fun x x_1 => x_1 x) n i)) → motive x hx
Equations
  • One or more equations did not get rendered due to their size.

Lemmas about additive closures of Subsemigroup.

theorem MulMemClass.mul_right_mem_add_closure {M : Type u_2} {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst : SetLike M R] [inst : MulMemClass M R] {S : M} {a : R} {b : R} (ha : a AddSubmonoid.closure S) (hb : b S) :

The product of an element of the additive closure of a multiplicative subsemigroup M and an element of M is contained in the additive closure of M.

theorem MulMemClass.mul_mem_add_closure {M : Type u_2} {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst : SetLike M R] [inst : MulMemClass M R] {S : M} {a : R} {b : R} (ha : a AddSubmonoid.closure S) (hb : b AddSubmonoid.closure S) :

The product of two elements of the additive closure of a submonoid M is an element of the additive closure of M.

theorem MulMemClass.mul_left_mem_add_closure {M : Type u_2} {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst : SetLike M R] [inst : MulMemClass M R] {S : M} {a : R} {b : R} (ha : a S) (hb : b AddSubmonoid.closure S) :

The product of an element of S and an element of the additive closure of a multiplicative submonoid S is contained in the additive closure of S.

theorem AddSubmonoid.mem_closure_pair {A : Type u_1} [inst : AddCommMonoid A] (a : A) (b : A) (c : A) :
c AddSubmonoid.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 Submonoid.mem_closure_pair {A : Type u_1} [inst : CommMonoid A] (a : A) (b : A) (c : A) :
c Submonoid.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 ofMul_image_powers_eq_multiples_ofMul {M : Type u_1} [inst : Monoid M] {x : M} :
Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))
theorem ofAdd_image_multiples_eq_powers_ofAdd {A : Type u_1} [inst : AddMonoid A] {x : A} :
Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))