Documentation

Mathlib.Algebra.Group.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_3} [AddMonoid M] [SetLike B M] [AddSubmonoidClass B M] {S : B} (l : List S) :
l.sum = (List.map Subtype.val l).sum
@[simp]
theorem SubmonoidClass.coe_list_prod {M : Type u_1} {B : Type u_3} [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} (l : List S) :
l.prod = (List.map Subtype.val l).prod
@[simp]
theorem AddSubmonoidClass.coe_multiset_sum {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset S) :
m.sum = (Multiset.map Subtype.val m).sum
@[simp]
theorem SubmonoidClass.coe_multiset_prod {B : Type u_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset S) :
m.prod = (Multiset.map Subtype.val m).prod
theorem AddSubmonoidClass.coe_finset_sum {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (f : ιS) (s : Finset ι) :
(∑ is, f i) = is, (f i)
theorem SubmonoidClass.coe_finset_prod {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (f : ιS) (s : Finset ι) :
(∏ is, f i) = is, (f i)
theorem list_sum_mem {M : Type u_1} {B : Type u_3} [AddMonoid M] [SetLike B M] [AddSubmonoidClass B M] {S : B} {l : List M} (hl : xl, x S) :
l.sum 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_3} [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} {l : List M} (hl : xl, x S) :
l.prod S

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

theorem multiset_sum_mem {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset M) (hm : am, a S) :
m.sum S

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

theorem multiset_prod_mem {B : Type u_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M) (hm : am, a S) :
m.prod S

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

theorem sum_mem {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ιM} (h : ct, f c S) :
ct, 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_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ιM} (h : ct, f c S) :
ct, 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} [AddMonoid M] (s : AddSubmonoid M) (l : List s) :
l.sum = (List.map Subtype.val l).sum
theorem Submonoid.coe_list_prod {M : Type u_1} [Monoid M] (s : Submonoid M) (l : List s) :
l.prod = (List.map Subtype.val l).prod
theorem AddSubmonoid.coe_multiset_sum {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset S) :
m.sum = (Multiset.map Subtype.val m).sum
theorem Submonoid.coe_multiset_prod {M : Type u_4} [CommMonoid M] (S : Submonoid M) (m : Multiset S) :
m.prod = (Multiset.map Subtype.val m).prod
@[simp]
theorem AddSubmonoid.coe_finset_sum {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] (S : AddSubmonoid M) (f : ιS) (s : Finset ι) :
(∑ is, f i) = is, (f i)
@[simp]
theorem Submonoid.coe_finset_prod {ι : Type u_4} {M : Type u_5} [CommMonoid M] (S : Submonoid M) (f : ιS) (s : Finset ι) :
(∏ is, f i) = is, (f i)
theorem AddSubmonoid.list_sum_mem {M : Type u_1} [AddMonoid M] (s : AddSubmonoid M) {l : List M} (hl : xl, x s) :
l.sum s

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

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

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

theorem AddSubmonoid.multiset_sum_mem {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M) (hm : am, a S) :
m.sum 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_4} [CommMonoid M] (S : Submonoid M) (m : Multiset M) (hm : am, a S) :
m.prod 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} [AddMonoid M] (S : AddSubmonoid M) (m : Multiset M) (comm : {x : M | x m}.Pairwise AddCommute) (h : xm, x S) :
m.noncommSum comm S
theorem Submonoid.multiset_noncommProd_mem {M : Type u_1} [Monoid M] (S : Submonoid M) (m : Multiset M) (comm : {x : M | x m}.Pairwise Commute) (h : xm, x S) :
m.noncommProd comm S
theorem AddSubmonoid.sum_mem {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) {ι : Type u_5} {t : Finset ι} {f : ιM} (h : ct, f c S) :
ct, 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_4} [CommMonoid M] (S : Submonoid M) {ι : Type u_5} {t : Finset ι} {f : ιM} (h : ct, f c S) :
ct, 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} [AddMonoid M] (S : AddSubmonoid M) {ι : Type u_4} (t : Finset ι) (f : ιM) (comm : (↑t).Pairwise fun (a b : ι) => AddCommute (f a) (f b)) (h : ct, f c S) :
t.noncommSum f comm S
theorem Submonoid.noncommProd_mem {M : Type u_1} [Monoid M] (S : Submonoid M) {ι : Type u_4} (t : Finset ι) (f : ιM) (comm : (↑t).Pairwise fun (a b : ι) => Commute (f a) (f b)) (h : ct, f c S) :
t.noncommProd f comm S
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
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.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.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.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 sS, x s
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 sS, x 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) = sS, 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) = sS, s
theorem AddSubmonoid.mem_sup_left {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} :
x Sx S T
theorem Submonoid.mem_sup_left {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} :
x Sx S T
theorem AddSubmonoid.mem_sup_right {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} :
x Tx S T
theorem Submonoid.mem_sup_right {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} :
x Tx S T
theorem AddSubmonoid.add_mem_sup {M : Type u_1} [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} [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_iSup_of_mem {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} {S : ιAddSubmonoid M} (i : ι) {x : M} :
x S ix iSup S
theorem Submonoid.mem_iSup_of_mem {M : Type u_1} [MulOneClass M] {ι : Sort u_4} {S : ιSubmonoid M} (i : ι) {x : M} :
x S ix iSup 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 sx sSup 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 sx sSup S
theorem AddSubmonoid.iSup_induction {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ιAddSubmonoid M) {C : MProp} {x : M} (hx : x ⨆ (i : ι), S i) (mem : ∀ (i : ι), xS i, C x) (one : C 0) (mul : ∀ (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.iSup_induction {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (S : ιSubmonoid M) {C : MProp} {x : M} (hx : x ⨆ (i : ι), S i) (mem : ∀ (i : ι), xS i, C x) (one : C 1) (mul : ∀ (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.iSup_induction' {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ιAddSubmonoid M) {C : (x : M) → x ⨆ (i : ι), S iProp} (mem : ∀ (i : ι) (x : M) (hxS : x S i), C x ) (one : C 0 ) (mul : ∀ (x y : M) (hx : x ⨆ (i : ι), S i) (hy : y ⨆ (i : ι), S i), C x hxC y hyC (x + y) ) {x : M} (hx : x ⨆ (i : ι), S i) :
C x hx

A dependent version of AddSubmonoid.iSup_induction.

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

A dependent version of Submonoid.iSup_induction.

theorem Submonoid.mem_closure_singleton {M : Type u_1} [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 AddSubmonoid.card_bot {M : Type u_1} [AddMonoid M] :
∀ {x : Fintype }, Fintype.card = 1
theorem Submonoid.card_bot {M : Type u_1} [Monoid M] :
∀ {x : Fintype }, Fintype.card = 1
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_le {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.eq_bot_of_card_eq {M : Type u_1} [Monoid M] {S : Submonoid M} [Fintype S] (h : Fintype.card S = 1) :
S =
theorem Submonoid.eq_bot_iff_card {M : Type u_1} [Monoid M] {S : Submonoid M} [Fintype S] :
theorem FreeAddMonoid.mrange_lift {M : Type u_1} [AddMonoid M] {α : Type u_4} (f : αM) :
theorem FreeMonoid.mrange_lift {M : Type u_1} [Monoid M] {α : Type u_4} (f : αM) :
theorem AddSubmonoid.closure_eq_mrange {M : Type u_1} [AddMonoid M] (s : Set M) :
AddSubmonoid.closure s = AddMonoidHom.mrange (FreeAddMonoid.lift Subtype.val)
theorem Submonoid.closure_eq_mrange {M : Type u_1} [Monoid M] (s : Set M) :
Submonoid.closure s = MonoidHom.mrange (FreeMonoid.lift Subtype.val)
theorem AddSubmonoid.closure_eq_image_sum {M : Type u_1} [AddMonoid M] (s : Set M) :
(AddSubmonoid.closure s) = List.sum '' {l : List M | xl, x s}
theorem Submonoid.closure_eq_image_prod {M : Type u_1} [Monoid M] (s : Set M) :
(Submonoid.closure s) = List.prod '' {l : List M | xl, x s}
theorem AddSubmonoid.exists_list_of_mem_closure {M : Type u_1} [AddMonoid M] {s : Set M} {x : M} (hx : x AddSubmonoid.closure s) :
∃ (l : List M), (∀ yl, y s) l.sum = x
theorem Submonoid.exists_list_of_mem_closure {M : Type u_1} [Monoid M] {s : Set M} {x : M} (hx : x Submonoid.closure s) :
∃ (l : List M), (∀ yl, 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 AddSubmonoid.closure s) :
∃ (l : Multiset M), (∀ yl, 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 Submonoid.closure s) :
∃ (l : Multiset M), (∀ yl, y s) l.prod = x
theorem AddSubmonoid.closure_induction_left {M : Type u_1} [AddMonoid M] {s : Set M} {p : (m : M) → m AddSubmonoid.closure sProp} (one : p 0 ) (mul_left : ∀ (x : M) (hx : x s) (y : M) (hy : y AddSubmonoid.closure s), p y hyp (x + y) ) {x : M} (h : x AddSubmonoid.closure s) :
p x h
theorem Submonoid.closure_induction_left {M : Type u_1} [Monoid M] {s : Set M} {p : (m : M) → m Submonoid.closure sProp} (one : p 1 ) (mul_left : ∀ (x : M) (hx : x s) (y : M) (hy : y Submonoid.closure s), p y hyp (x * y) ) {x : M} (h : x Submonoid.closure s) :
p x h
theorem AddSubmonoid.induction_of_closure_eq_top_left {M : Type u_1} [AddMonoid M] {s : Set M} {p : MProp} (hs : AddSubmonoid.closure s = ) (x : M) (one : p 0) (mul : xs, ∀ (y : M), p yp (x + y)) :
p x
theorem Submonoid.induction_of_closure_eq_top_left {M : Type u_1} [Monoid M] {s : Set M} {p : MProp} (hs : Submonoid.closure s = ) (x : M) (one : p 1) (mul : xs, ∀ (y : M), p yp (x * y)) :
p x
theorem AddSubmonoid.closure_induction_right {M : Type u_1} [AddMonoid M] {s : Set M} {p : (m : M) → m AddSubmonoid.closure sProp} (one : p 0 ) (mul_right : ∀ (x : M) (hx : x AddSubmonoid.closure s) (y : M) (hy : y s), p x hxp (x + y) ) {x : M} (h : x AddSubmonoid.closure s) :
p x h
theorem Submonoid.closure_induction_right {M : Type u_1} [Monoid M] {s : Set M} {p : (m : M) → m Submonoid.closure sProp} (one : p 1 ) (mul_right : ∀ (x : M) (hx : x Submonoid.closure s) (y : M) (hy : y s), p x hxp (x * y) ) {x : M} (h : x Submonoid.closure s) :
p x h
theorem AddSubmonoid.induction_of_closure_eq_top_right {M : Type u_1} [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} [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} [Monoid M] (n : M) :

The submonoid generated by an element.

Equations
Instances For
    @[simp]
    theorem Submonoid.mem_powers {M : Type u_1} [Monoid M] (n : M) :
    theorem Submonoid.coe_powers {M : Type u_1} [Monoid M] (x : M) :
    (Submonoid.powers x) = Set.range fun (n : ) => x ^ n
    theorem Submonoid.mem_powers_iff {M : Type u_1} [Monoid M] (x : M) (z : M) :
    x Submonoid.powers z ∃ (n : ), z ^ n = x
    noncomputable instance Submonoid.decidableMemPowers {M : Type u_1} [Monoid M] {a : M} :
    Equations
    noncomputable instance Submonoid.fintypePowers {M : Type u_1} [Monoid M] {a : M} [Fintype M] :
    Equations
    theorem Submonoid.powers_le {M : Type u_1} [Monoid M] {n : M} {P : Submonoid M} :
    @[simp]
    @[reducible, inline]
    abbrev Submonoid.groupPowers {M : Type u_1} [Monoid M] {x : M} {n : } (hpos : 0 < n) (hx : x ^ n = 1) :

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

    Equations
    Instances For
      @[simp]
      theorem Submonoid.pow_coe {M : Type u_1} [Monoid M] (n : M) (m : ) :
      (Submonoid.pow n m) = n ^ m
      def Submonoid.pow {M : Type u_1} [Monoid M] (n : M) (m : ) :

      Exponentiation map from natural numbers to powers.

      Equations
      Instances For
        theorem Submonoid.pow_apply {M : Type u_1} [Monoid M] (n : M) (m : ) :
        Submonoid.pow n m = n ^ m,
        def Submonoid.log {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (p : (Submonoid.powers n)) :

        Logarithms from powers to natural numbers.

        Equations
        Instances For
          @[simp]
          theorem Submonoid.pow_log_eq_self {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (p : (Submonoid.powers 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 : ) :
          @[simp]
          theorem Submonoid.powLogEquiv_apply {M : Type u_1} [Monoid M] [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} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ) => n ^ m) (m : (Submonoid.powers n)) :
          (Submonoid.powLogEquiv h).symm m = Multiplicative.ofAdd (Submonoid.log m)
          def Submonoid.powLogEquiv {M : Type u_1} [Monoid M] [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.
          Instances For
            theorem Submonoid.log_mul {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun (m : ) => n ^ m) (x : (Submonoid.powers n)) (y : (Submonoid.powers n)) :
            theorem Submonoid.log_pow_int_eq_self {x : } (h : 1 < x.natAbs) (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) :
            theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_1 {M : Type u_1} [AddMonoid M] {s : Set M} (hcomm : as, bs, a + b = b + a) (x : (AddSubmonoid.closure s)) (y : (AddSubmonoid.closure s)) :
            x + y = y + x
            def AddSubmonoid.closureAddCommMonoidOfComm {M : Type u_1} [AddMonoid M] {s : Set M} (hcomm : as, bs, a + b = b + a) :

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

            Equations
            Instances For
              def Submonoid.closureCommMonoidOfComm {M : Type u_1} [Monoid M] {s : Set M} (hcomm : as, bs, a * b = b * a) :

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

              Equations
              Instances For
                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 : xs, ∀ (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)) :
                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 : xs, ∀ (y : N) (z : α), (x y) z = x y z) :
                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 : xs, ∀ (y : N) (z : α), x +ᵥ (y +ᵥ z) = y +ᵥ (x +ᵥ z)) :
                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 : xs, ∀ (y : N) (z : α), x y z = y x z) :
                theorem AddSubmonoid.sup_eq_range {N : Type u_4} [AddCommMonoid N] (s : AddSubmonoid N) (t : AddSubmonoid N) :
                s t = AddMonoidHom.mrange (s.subtype.coprod t.subtype)
                theorem Submonoid.sup_eq_range {N : Type u_4} [CommMonoid N] (s : Submonoid N) (t : Submonoid N) :
                s t = MonoidHom.mrange (s.subtype.coprod t.subtype)
                theorem AddSubmonoid.mem_sup {N : Type u_4} [AddCommMonoid N] {s : AddSubmonoid N} {t : AddSubmonoid N} {x : N} :
                x s t ys, zt, y + z = x
                theorem Submonoid.mem_sup {N : Type u_4} [CommMonoid N] {s : Submonoid N} {t : Submonoid N} {x : N} :
                x s t ys, zt, y * z = x
                theorem AddSubmonoid.mem_closure_singleton {A : Type u_2} [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_2} [AddMonoid A] (x : A) :

                The additive submonoid generated by an element.

                Equations
                Instances For
                  @[simp]
                  theorem AddSubmonoid.coe_multiples {M : Type u_1} [AddMonoid M] (x : M) :
                  (AddSubmonoid.multiples x) = Set.range fun (n : ) => n x
                  theorem AddSubmonoid.mem_multiples_iff {M : Type u_1} [AddMonoid M] (x : M) (z : M) :
                  x AddSubmonoid.multiples z ∃ (n : ), n z = x
                  noncomputable instance AddSubmonoid.decidableMemMultiples {M : Type u_1} [AddMonoid M] {a : M} :
                  Equations
                  noncomputable instance AddSubmonoid.fintypeMultiples {M : Type u_1} [AddMonoid M] {a : M} [Fintype M] :
                  Equations
                  theorem AddSubmonoid.addGroupMultiples.proof_5 {M : Type u_1} [AddMonoid M] {x : M} {n : } (hpos : 0 < n) (hx : n x✝ = 0) (m : ) (x : (AddSubmonoid.multiples x✝)) :
                  (fun (z : ) (x : (AddSubmonoid.multiples x✝)) => z.natMod n x) (Int.negSucc m) x = -(fun (z : ) (x : (AddSubmonoid.multiples x✝)) => z.natMod n x) (↑m.succ) x
                  theorem AddSubmonoid.addGroupMultiples.proof_6 {M : Type u_1} [AddMonoid M] {x : M} {n : } (hpos : 0 < n) (hx : n x = 0) (y : (AddSubmonoid.multiples x)) :
                  -y + y = 0
                  theorem AddSubmonoid.addGroupMultiples.proof_4 {M : Type u_1} [AddMonoid M] {x : M} {n : } (hx : n x✝ = 0) (m : ) (x : (AddSubmonoid.multiples x✝)) :
                  (fun (z : ) (x : (AddSubmonoid.multiples x✝)) => z.natMod n x) (Int.ofNat m.succ) x = (fun (z : ) (x : (AddSubmonoid.multiples x✝)) => z.natMod n x) (Int.ofNat m) x + x
                  @[reducible, inline]
                  abbrev AddSubmonoid.addGroupMultiples {M : Type u_1} [AddMonoid M] {x : M} {n : } (hpos : 0 < n) (hx : n x = 0) :

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

                  Equations
                  Instances For
                    theorem AddSubmonoid.addGroupMultiples.proof_2 {M : Type u_1} [AddMonoid M] {x : M} {n : } :
                    ∀ (a b : (AddSubmonoid.multiples x)), a - b = a - b

                    Lemmas about additive closures of Subsemigroup.

                    theorem MulMemClass.mul_right_mem_add_closure {M : Type u_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] [SetLike M R] [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_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] [SetLike M R] [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_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] [SetLike M R] [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_4} [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_4} [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} [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))

                    The submonoid of primal elements in a cancellative commutative monoid with zero.

                    Equations
                    Instances For