Documentation

Mathlib.Algebra.Group.Submonoid.Basic

Submonoids: definition and CompleteLattice structure #

This file defines bundled multiplicative and additive submonoids. We also define a CompleteLattice structure on Submonoids, define the closure of a set as the minimal submonoid that includes this set, and prove a few results about extending properties from a dense set (i.e. a set with closure s = ⊤) to the whole monoid, see Submonoid.dense_induction and MonoidHom.ofClosureEqTopLeft/MonoidHom.ofClosureEqTopRight.

Main definitions #

For each of the following definitions in the Submonoid namespace, there is a corresponding definition in the AddSubmonoid namespace.

Implementation notes #

Submonoid inclusion is denoted rather than , although is defined as membership of a submonoid's underlying set.

Note that Submonoid M does not actually require Monoid M, instead requiring only the weaker MulOneClass M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers. Submonoid is implemented by extending Subsemigroup requiring one_mem'.

Tags #

submonoid, submonoids

class OneMemClass (S : Type u_4) (M : Type u_5) [One M] [SetLike S M] :

OneMemClass S M says S is a type of subsets s ≤ M, such that 1 ∈ s for all s.

  • one_mem : ∀ (s : S), 1 s

    By definition, if we have OneMemClass S M, we have 1 ∈ s for all s : S.

Instances
    theorem OneMemClass.one_mem {S : Type u_4} {M : Type u_5} :
    ∀ {inst : One M} {inst_1 : SetLike S M} [self : OneMemClass S M] (s : S), 1 s

    By definition, if we have OneMemClass S M, we have 1 ∈ s for all s : S.

    class ZeroMemClass (S : Type u_4) (M : Type u_5) [Zero M] [SetLike S M] :

    ZeroMemClass S M says S is a type of subsets s ≤ M, such that 0 ∈ s for all s.

    • zero_mem : ∀ (s : S), 0 s

      By definition, if we have ZeroMemClass S M, we have 0 ∈ s for all s : S.

    Instances
      theorem ZeroMemClass.zero_mem {S : Type u_4} {M : Type u_5} :
      ∀ {inst : Zero M} {inst_1 : SetLike S M} [self : ZeroMemClass S M] (s : S), 0 s

      By definition, if we have ZeroMemClass S M, we have 0 ∈ s for all s : S.

      structure Submonoid (M : Type u_4) [MulOneClass M] extends Subsemigroup :
      Type u_4

      A submonoid of a monoid M is a subset containing 1 and closed under multiplication.

      • carrier : Set M
      • mul_mem' : ∀ {a b : M}, a self.carrierb self.carriera * b self.carrier
      • one_mem' : 1 self.carrier

        A submonoid contains 1.

      Instances For
        theorem Submonoid.one_mem' {M : Type u_4} [MulOneClass M] (self : Submonoid M) :
        1 self.carrier

        A submonoid contains 1.

        class SubmonoidClass (S : Type u_4) (M : Type u_5) [MulOneClass M] [SetLike S M] extends MulMemClass , OneMemClass :

        SubmonoidClass S M says S is a type of subsets s ≤ M that contain 1 and are closed under (*)

          Instances
            structure AddSubmonoid (M : Type u_4) [AddZeroClass M] extends AddSubsemigroup :
            Type u_4

            An additive submonoid of an additive monoid M is a subset containing 0 and closed under addition.

            • carrier : Set M
            • add_mem' : ∀ {a b : M}, a self.carrierb self.carriera + b self.carrier
            • zero_mem' : 0 self.carrier

              An additive submonoid contains 0.

            Instances For
              theorem AddSubmonoid.zero_mem' {M : Type u_4} [AddZeroClass M] (self : AddSubmonoid M) :
              0 self.carrier

              An additive submonoid contains 0.

              class AddSubmonoidClass (S : Type u_4) (M : Type u_5) [AddZeroClass M] [SetLike S M] extends AddMemClass , ZeroMemClass :

              AddSubmonoidClass S M says S is a type of subsets s ≤ M that contain 0 and are closed under (+)

                Instances
                  theorem nsmul_mem {M : Type u_4} {A : Type u_5} [AddMonoid M] [SetLike A M] [AddSubmonoidClass A M] {S : A} {x : M} (hx : x S) (n : ) :
                  n x S
                  theorem pow_mem {M : Type u_4} {A : Type u_5} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M} (hx : x S) (n : ) :
                  x ^ n S
                  Equations
                  • AddSubmonoid.instSetLike = { coe := fun (s : AddSubmonoid M) => s.carrier, coe_injective' := }
                  theorem AddSubmonoid.instSetLike.proof_1 {M : Type u_1} [AddZeroClass M] (p : AddSubmonoid M) (q : AddSubmonoid M) (h : (fun (s : AddSubmonoid M) => s.carrier) p = (fun (s : AddSubmonoid M) => s.carrier) q) :
                  p = q
                  Equations
                  • Submonoid.instSetLike = { coe := fun (s : Submonoid M) => s.carrier, coe_injective' := }
                  Equations
                  • =
                  @[simp]
                  theorem AddSubmonoid.mem_toSubsemigroup {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {x : M} :
                  x s.toAddSubsemigroup x s
                  @[simp]
                  theorem Submonoid.mem_toSubsemigroup {M : Type u_1} [MulOneClass M] {s : Submonoid M} {x : M} :
                  x s.toSubsemigroup x s
                  theorem AddSubmonoid.mem_carrier {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {x : M} :
                  x s.carrier x s
                  theorem Submonoid.mem_carrier {M : Type u_1} [MulOneClass M] {s : Submonoid M} {x : M} :
                  x s.carrier x s
                  @[simp]
                  theorem AddSubmonoid.mem_mk {M : Type u_1} [AddZeroClass M] {s : AddSubsemigroup M} {x : M} (h_one : 0 s.carrier) :
                  x { toAddSubsemigroup := s, zero_mem' := h_one } x s
                  @[simp]
                  theorem Submonoid.mem_mk {M : Type u_1} [MulOneClass M] {s : Subsemigroup M} {x : M} (h_one : 1 s.carrier) :
                  x { toSubsemigroup := s, one_mem' := h_one } x s
                  @[simp]
                  theorem AddSubmonoid.coe_set_mk {M : Type u_1} [AddZeroClass M] {s : AddSubsemigroup M} (h_one : 0 s.carrier) :
                  { toAddSubsemigroup := s, zero_mem' := h_one } = s
                  @[simp]
                  theorem Submonoid.coe_set_mk {M : Type u_1} [MulOneClass M] {s : Subsemigroup M} (h_one : 1 s.carrier) :
                  { toSubsemigroup := s, one_mem' := h_one } = s
                  @[simp]
                  theorem AddSubmonoid.mk_le_mk {M : Type u_1} [AddZeroClass M] {s : AddSubsemigroup M} {t : AddSubsemigroup M} (h_one : 0 s.carrier) (h_one' : 0 t.carrier) :
                  { toAddSubsemigroup := s, zero_mem' := h_one } { toAddSubsemigroup := t, zero_mem' := h_one' } s t
                  @[simp]
                  theorem Submonoid.mk_le_mk {M : Type u_1} [MulOneClass M] {s : Subsemigroup M} {t : Subsemigroup M} (h_one : 1 s.carrier) (h_one' : 1 t.carrier) :
                  { toSubsemigroup := s, one_mem' := h_one } { toSubsemigroup := t, one_mem' := h_one' } s t
                  theorem AddSubmonoid.ext {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : ∀ (x : M), x S x T) :
                  S = T

                  Two AddSubmonoids are equal if they have the same elements.

                  theorem AddSubmonoid.ext_iff {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} :
                  S = T ∀ (x : M), x S x T
                  theorem Submonoid.ext_iff {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} :
                  S = T ∀ (x : M), x S x T
                  theorem Submonoid.ext {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : ∀ (x : M), x S x T) :
                  S = T

                  Two submonoids are equal if they have the same elements.

                  theorem AddSubmonoid.copy.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = S) :
                  ∀ {a b : M}, a sb sa + b s
                  theorem AddSubmonoid.copy.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = S) :
                  0 s
                  def AddSubmonoid.copy {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = S) :

                  Copy an additive submonoid replacing carrier with a set that is equal to it.

                  Equations
                  • S.copy s hs = { carrier := s, add_mem' := , zero_mem' := }
                  Instances For
                    def Submonoid.copy {M : Type u_1} [MulOneClass M] (S : Submonoid M) (s : Set M) (hs : s = S) :

                    Copy a submonoid replacing carrier with a set that is equal to it.

                    Equations
                    • S.copy s hs = { carrier := s, mul_mem' := , one_mem' := }
                    Instances For
                      @[simp]
                      theorem AddSubmonoid.coe_copy {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {s : Set M} (hs : s = S) :
                      (S.copy s hs) = s
                      @[simp]
                      theorem Submonoid.coe_copy {M : Type u_1} [MulOneClass M] {S : Submonoid M} {s : Set M} (hs : s = S) :
                      (S.copy s hs) = s
                      theorem AddSubmonoid.copy_eq {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {s : Set M} (hs : s = S) :
                      S.copy s hs = S
                      theorem Submonoid.copy_eq {M : Type u_1} [MulOneClass M] {S : Submonoid M} {s : Set M} (hs : s = S) :
                      S.copy s hs = S
                      theorem AddSubmonoid.zero_mem {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                      0 S

                      An AddSubmonoid contains the monoid's 0.

                      theorem Submonoid.one_mem {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                      1 S

                      A submonoid contains the monoid's 1.

                      theorem AddSubmonoid.add_mem {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) {x : M} {y : M} :
                      x Sy Sx + y S

                      An AddSubmonoid is closed under addition.

                      theorem Submonoid.mul_mem {M : Type u_1} [MulOneClass M] (S : Submonoid M) {x : M} {y : M} :
                      x Sy Sx * y S

                      A submonoid is closed under multiplication.

                      theorem AddSubmonoid.instTop.proof_1 {M : Type u_1} [AddZeroClass M] :
                      ∀ {a b : M}, a Set.univb Set.univa + b Set.univ

                      The additive submonoid M of the AddMonoid M.

                      Equations
                      • AddSubmonoid.instTop = { top := { carrier := Set.univ, add_mem' := , zero_mem' := } }
                      theorem AddSubmonoid.instTop.proof_2 {M : Type u_1} [AddZeroClass M] :
                      0 Set.univ
                      instance Submonoid.instTop {M : Type u_1} [MulOneClass M] :

                      The submonoid M of the monoid M.

                      Equations
                      • Submonoid.instTop = { top := { carrier := Set.univ, mul_mem' := , one_mem' := } }
                      theorem AddSubmonoid.instBot.proof_1 {M : Type u_1} [AddZeroClass M] :
                      ∀ {a b : M}, a {0}b {0}a + b {0}

                      The trivial AddSubmonoid {0} of an AddMonoid M.

                      Equations
                      • AddSubmonoid.instBot = { bot := { carrier := {0}, add_mem' := , zero_mem' := } }
                      instance Submonoid.instBot {M : Type u_1} [MulOneClass M] :

                      The trivial submonoid {1} of a monoid M.

                      Equations
                      • Submonoid.instBot = { bot := { carrier := {1}, mul_mem' := , one_mem' := } }
                      Equations
                      • AddSubmonoid.instInhabited = { default := }
                      Equations
                      • Submonoid.instInhabited = { default := }
                      @[simp]
                      theorem AddSubmonoid.mem_bot {M : Type u_1} [AddZeroClass M] {x : M} :
                      x x = 0
                      @[simp]
                      theorem Submonoid.mem_bot {M : Type u_1} [MulOneClass M] {x : M} :
                      x x = 1
                      @[simp]
                      theorem AddSubmonoid.mem_top {M : Type u_1} [AddZeroClass M] (x : M) :
                      @[simp]
                      theorem Submonoid.mem_top {M : Type u_1} [MulOneClass M] (x : M) :
                      @[simp]
                      theorem AddSubmonoid.coe_top {M : Type u_1} [AddZeroClass M] :
                      = Set.univ
                      @[simp]
                      theorem Submonoid.coe_top {M : Type u_1} [MulOneClass M] :
                      = Set.univ
                      @[simp]
                      theorem AddSubmonoid.coe_bot {M : Type u_1} [AddZeroClass M] :
                      = {0}
                      @[simp]
                      theorem Submonoid.coe_bot {M : Type u_1} [MulOneClass M] :
                      = {1}

                      The inf of two AddSubmonoids is their intersection.

                      Equations
                      • AddSubmonoid.instInf = { inf := fun (S₁ S₂ : AddSubmonoid M) => { carrier := S₁ S₂, add_mem' := , zero_mem' := } }
                      theorem AddSubmonoid.instInf.proof_1 {M : Type u_1} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
                      ∀ {a b : M}, a S₁ S₂b S₁ S₂a + b S₁ S₂
                      theorem AddSubmonoid.instInf.proof_2 {M : Type u_1} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
                      0 S₁ 0 S₂
                      instance Submonoid.instInf {M : Type u_1} [MulOneClass M] :

                      The inf of two submonoids is their intersection.

                      Equations
                      • Submonoid.instInf = { inf := fun (S₁ S₂ : Submonoid M) => { carrier := S₁ S₂, mul_mem' := , one_mem' := } }
                      @[simp]
                      theorem AddSubmonoid.coe_inf {M : Type u_1} [AddZeroClass M] (p : AddSubmonoid M) (p' : AddSubmonoid M) :
                      (p p') = p p'
                      @[simp]
                      theorem Submonoid.coe_inf {M : Type u_1} [MulOneClass M] (p : Submonoid M) (p' : Submonoid M) :
                      (p p') = p p'
                      @[simp]
                      theorem AddSubmonoid.mem_inf {M : Type u_1} [AddZeroClass M] {p : AddSubmonoid M} {p' : AddSubmonoid M} {x : M} :
                      x p p' x p x p'
                      @[simp]
                      theorem Submonoid.mem_inf {M : Type u_1} [MulOneClass M] {p : Submonoid M} {p' : Submonoid M} {x : M} :
                      x p p' x p x p'
                      Equations
                      • AddSubmonoid.instInfSet = { sInf := fun (s : Set (AddSubmonoid M)) => { carrier := ts, t, add_mem' := , zero_mem' := } }
                      theorem AddSubmonoid.instInfSet.proof_1 {M : Type u_1} [AddZeroClass M] (s : Set (AddSubmonoid M)) :
                      ∀ {a b : M}, a ts, tb ts, ta + b xs, x
                      theorem AddSubmonoid.instInfSet.proof_2 {M : Type u_1} [AddZeroClass M] (s : Set (AddSubmonoid M)) :
                      0 xs, x
                      Equations
                      • Submonoid.instInfSet = { sInf := fun (s : Set (Submonoid M)) => { carrier := ts, t, mul_mem' := , one_mem' := } }
                      @[simp]
                      theorem AddSubmonoid.coe_sInf {M : Type u_1} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
                      (sInf S) = sS, s
                      @[simp]
                      theorem Submonoid.coe_sInf {M : Type u_1} [MulOneClass M] (S : Set (Submonoid M)) :
                      (sInf S) = sS, s
                      theorem AddSubmonoid.mem_sInf {M : Type u_1} [AddZeroClass M] {S : Set (AddSubmonoid M)} {x : M} :
                      x sInf S pS, x p
                      theorem Submonoid.mem_sInf {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} {x : M} :
                      x sInf S pS, x p
                      theorem AddSubmonoid.mem_iInf {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} {S : ιAddSubmonoid M} {x : M} :
                      x ⨅ (i : ι), S i ∀ (i : ι), x S i
                      theorem Submonoid.mem_iInf {M : Type u_1} [MulOneClass M] {ι : Sort u_4} {S : ιSubmonoid M} {x : M} :
                      x ⨅ (i : ι), S i ∀ (i : ι), x S i
                      @[simp]
                      theorem AddSubmonoid.coe_iInf {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} {S : ιAddSubmonoid M} :
                      (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                      @[simp]
                      theorem Submonoid.coe_iInf {M : Type u_1} [MulOneClass M] {ι : Sort u_4} {S : ιSubmonoid M} :
                      (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                      theorem AddSubmonoid.instCompleteLattice.proof_13 {M : Type u_1} [AddZeroClass M] (s : Set (AddSubmonoid M)) (a : AddSubmonoid M) :
                      (∀ bs, b a)sSup s a
                      theorem AddSubmonoid.instCompleteLattice.proof_9 {M : Type u_1} [AddZeroClass M] :
                      ∀ (x x_1 : AddSubmonoid M) (x_2 : M), x_2 x x_2 x_1x_2 x
                      theorem AddSubmonoid.instCompleteLattice.proof_10 {M : Type u_1} [AddZeroClass M] :
                      ∀ (x x_1 : AddSubmonoid M) (x_2 : M), x_2 x x_2 x_1x_2 x_1
                      theorem AddSubmonoid.instCompleteLattice.proof_8 {M : Type u_1} [AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) (c : AddSubmonoid M) :
                      a cb ca b c
                      theorem AddSubmonoid.instCompleteLattice.proof_5 {M : Type u_1} [AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) :
                      a bb aa = b
                      theorem AddSubmonoid.instCompleteLattice.proof_15 {M : Type u_1} [AddZeroClass M] (s : Set (AddSubmonoid M)) (a : AddSubmonoid M) :
                      (∀ bs, a b)a sInf s

                      The AddSubmonoids of an AddMonoid form a complete lattice.

                      Equations
                      theorem AddSubmonoid.instCompleteLattice.proof_3 {M : Type u_1} [AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) (c : AddSubmonoid M) :
                      a bb ca c
                      theorem AddSubmonoid.instCompleteLattice.proof_11 {M : Type u_1} [AddZeroClass M] :
                      ∀ (x x_1 x_2 : AddSubmonoid M), x x_1x x_2x_3x, x_3 x_1 x_3 x_2

                      Submonoids of a monoid form a complete lattice.

                      Equations
                      Equations
                      • AddSubmonoid.instUniqueOfSubsingleton = { default := , uniq := }
                      Equations
                      • Submonoid.instUniqueOfSubsingleton = { default := , uniq := }
                      Equations
                      • =

                      The AddSubmonoid generated by a set

                      Equations
                      Instances For
                        def Submonoid.closure {M : Type u_1} [MulOneClass M] (s : Set M) :

                        The Submonoid generated by a set.

                        Equations
                        Instances For
                          theorem AddSubmonoid.mem_closure {M : Type u_1} [AddZeroClass M] {s : Set M} {x : M} :
                          x AddSubmonoid.closure s ∀ (S : AddSubmonoid M), s Sx S
                          theorem Submonoid.mem_closure {M : Type u_1} [MulOneClass M] {s : Set M} {x : M} :
                          x Submonoid.closure s ∀ (S : Submonoid M), s Sx S
                          @[simp]

                          The AddSubmonoid generated by a set includes the set.

                          @[simp]
                          theorem Submonoid.subset_closure {M : Type u_1} [MulOneClass M] {s : Set M} :

                          The submonoid generated by a set includes the set.

                          theorem AddSubmonoid.not_mem_of_not_mem_closure {M : Type u_1} [AddZeroClass M] {s : Set M} {P : M} (hP : PAddSubmonoid.closure s) :
                          Ps
                          theorem Submonoid.not_mem_of_not_mem_closure {M : Type u_1} [MulOneClass M] {s : Set M} {P : M} (hP : PSubmonoid.closure s) :
                          Ps
                          @[simp]
                          theorem AddSubmonoid.closure_le {M : Type u_1} [AddZeroClass M] {s : Set M} {S : AddSubmonoid M} :

                          An additive submonoid S includes closure s if and only if it includes s

                          @[simp]
                          theorem Submonoid.closure_le {M : Type u_1} [MulOneClass M] {s : Set M} {S : Submonoid M} :

                          A submonoid S includes closure s if and only if it includes s.

                          theorem AddSubmonoid.closure_mono {M : Type u_1} [AddZeroClass M] ⦃s : Set M ⦃t : Set M (h : s t) :

                          Additive submonoid closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t

                          theorem Submonoid.closure_mono {M : Type u_1} [MulOneClass M] ⦃s : Set M ⦃t : Set M (h : s t) :

                          Submonoid closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

                          theorem AddSubmonoid.closure_eq_of_le {M : Type u_1} [AddZeroClass M] {s : Set M} {S : AddSubmonoid M} (h₁ : s S) (h₂ : S AddSubmonoid.closure s) :
                          theorem Submonoid.closure_eq_of_le {M : Type u_1} [MulOneClass M] {s : Set M} {S : Submonoid M} (h₁ : s S) (h₂ : S Submonoid.closure s) :
                          theorem AddSubmonoid.closure_induction {M : Type u_1} [AddZeroClass M] {s : Set M} {p : MProp} {x : M} (h : x AddSubmonoid.closure s) (mem : xs, p x) (one : p 0) (mul : ∀ (x y : M), p xp yp (x + y)) :
                          p x

                          An induction principle for additive closure membership. If p holds for 0 and all elements of s, and is preserved under addition, then p holds for all elements of the additive closure of s.

                          theorem Submonoid.closure_induction {M : Type u_1} [MulOneClass M] {s : Set M} {p : MProp} {x : M} (h : x Submonoid.closure s) (mem : xs, p x) (one : p 1) (mul : ∀ (x y : M), p xp yp (x * y)) :
                          p x

                          An induction principle for closure membership. If p holds for 1 and all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

                          theorem AddSubmonoid.closure_induction' {M : Type u_1} [AddZeroClass M] (s : Set M) {p : (x : M) → x AddSubmonoid.closure sProp} (mem : ∀ (x : M) (h : x s), p x ) (one : p 0 ) (mul : ∀ (x : M) (hx : x AddSubmonoid.closure s) (y : M) (hy : y AddSubmonoid.closure s), p x hxp y hyp (x + y) ) {x : M} (hx : x AddSubmonoid.closure s) :
                          p x hx

                          A dependent version of AddSubmonoid.closure_induction.

                          theorem Submonoid.closure_induction' {M : Type u_1} [MulOneClass M] (s : Set M) {p : (x : M) → x Submonoid.closure sProp} (mem : ∀ (x : M) (h : x s), p x ) (one : p 1 ) (mul : ∀ (x : M) (hx : x Submonoid.closure s) (y : M) (hy : y Submonoid.closure s), p x hxp y hyp (x * y) ) {x : M} (hx : x Submonoid.closure s) :
                          p x hx

                          A dependent version of Submonoid.closure_induction.

                          theorem AddSubmonoid.closure_induction₂ {M : Type u_1} [AddZeroClass M] {s : Set M} {p : MMProp} {x : M} {y : M} (hx : x AddSubmonoid.closure s) (hy : y AddSubmonoid.closure s) (Hs : xs, ys, p x y) (H1_left : ∀ (x : M), p 0 x) (H1_right : ∀ (x : M), p x 0) (Hmul_left : ∀ (x y z : M), p x zp y zp (x + y) z) (Hmul_right : ∀ (x y z : M), p z xp z yp z (x + y)) :
                          p x y

                          An induction principle for additive closure membership for predicates with two arguments.

                          theorem Submonoid.closure_induction₂ {M : Type u_1} [MulOneClass M] {s : Set M} {p : MMProp} {x : M} {y : M} (hx : x Submonoid.closure s) (hy : y Submonoid.closure s) (Hs : xs, ys, p x y) (H1_left : ∀ (x : M), p 1 x) (H1_right : ∀ (x : M), p x 1) (Hmul_left : ∀ (x y z : M), p x zp y zp (x * y) z) (Hmul_right : ∀ (x y z : M), p z xp z yp z (x * y)) :
                          p x y

                          An induction principle for closure membership for predicates with two arguments.

                          theorem AddSubmonoid.dense_induction {M : Type u_1} [AddZeroClass M] {p : MProp} (x : M) {s : Set M} (hs : AddSubmonoid.closure s = ) (mem : xs, p x) (one : p 0) (mul : ∀ (x y : M), p xp yp (x + y)) :
                          p x

                          If s is a dense set in an additive monoid M, AddSubmonoid.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, verify p 0, and verify that p x and p y imply p (x + y).

                          theorem Submonoid.dense_induction {M : Type u_1} [MulOneClass M] {p : MProp} (x : M) {s : Set M} (hs : Submonoid.closure s = ) (mem : xs, p x) (one : p 1) (mul : ∀ (x y : M), p xp yp (x * y)) :
                          p x

                          If s is a dense set in a monoid M, Submonoid.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, verify p 1, and verify that p x and p y imply p (x * y).

                          The Submonoid.closure of a set is the union of {1} and its Subsemigroup.closure.

                          theorem AddSubmonoid.gi.proof_2 (M : Type u_1) [AddZeroClass M] :
                          ∀ (x : Set M) (x_1 : (AddSubmonoid.closure x) x), (fun (s : Set M) (x : (AddSubmonoid.closure s) s) => AddSubmonoid.closure s) x x_1 = (fun (s : Set M) (x : (AddSubmonoid.closure s) s) => AddSubmonoid.closure s) x x_1
                          theorem AddSubmonoid.gi.proof_1 (M : Type u_1) [AddZeroClass M] :
                          ∀ (x : AddSubmonoid M), x (AddSubmonoid.closure x)
                          def AddSubmonoid.gi (M : Type u_1) [AddZeroClass M] :
                          GaloisInsertion AddSubmonoid.closure SetLike.coe

                          closure forms a Galois insertion with the coercion to set.

                          Equations
                          Instances For
                            def Submonoid.gi (M : Type u_1) [MulOneClass M] :
                            GaloisInsertion Submonoid.closure SetLike.coe

                            closure forms a Galois insertion with the coercion to set.

                            Equations
                            Instances For
                              @[simp]

                              Additive closure of an additive submonoid S equals S

                              @[simp]
                              theorem Submonoid.closure_eq {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

                              Closure of a submonoid S equals S.

                              @[simp]
                              theorem Submonoid.sup_eq_closure {M : Type u_1} [MulOneClass M] (N : Submonoid M) (N' : Submonoid M) :
                              N N' = Submonoid.closure (N N')
                              theorem AddSubmonoid.closure_iUnion {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (s : ιSet M) :
                              AddSubmonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι), AddSubmonoid.closure (s i)
                              theorem Submonoid.closure_iUnion {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (s : ιSet M) :
                              Submonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Submonoid.closure (s i)
                              theorem AddSubmonoid.mem_iSup {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (p : ιAddSubmonoid M) {m : M} :
                              m ⨆ (i : ι), p i ∀ (N : AddSubmonoid M), (∀ (i : ι), p i N)m N
                              theorem Submonoid.mem_iSup {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (p : ιSubmonoid M) {m : M} :
                              m ⨆ (i : ι), p i ∀ (N : Submonoid M), (∀ (i : ι), p i N)m N
                              theorem AddSubmonoid.iSup_eq_closure {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (p : ιAddSubmonoid M) :
                              ⨆ (i : ι), p i = AddSubmonoid.closure (⋃ (i : ι), (p i))
                              theorem Submonoid.iSup_eq_closure {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (p : ιSubmonoid M) :
                              ⨆ (i : ι), p i = Submonoid.closure (⋃ (i : ι), (p i))
                              theorem AddSubmonoid.disjoint_def {M : Type u_1} [AddZeroClass M] {p₁ : AddSubmonoid M} {p₂ : AddSubmonoid M} :
                              Disjoint p₁ p₂ ∀ {x : M}, x p₁x p₂x = 0
                              theorem Submonoid.disjoint_def {M : Type u_1} [MulOneClass M] {p₁ : Submonoid M} {p₂ : Submonoid M} :
                              Disjoint p₁ p₂ ∀ {x : M}, x p₁x p₂x = 1
                              theorem AddSubmonoid.disjoint_def' {M : Type u_1} [AddZeroClass M] {p₁ : AddSubmonoid M} {p₂ : AddSubmonoid M} :
                              Disjoint p₁ p₂ ∀ {x y : M}, x p₁y p₂x = yx = 0
                              theorem Submonoid.disjoint_def' {M : Type u_1} [MulOneClass M] {p₁ : Submonoid M} {p₂ : Submonoid M} :
                              Disjoint p₁ p₂ ∀ {x y : M}, x p₁y p₂x = yx = 1
                              theorem AddMonoidHom.eqLocusM.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : M →+ N) :
                              0 { carrier := {x : M | f x = g x}, add_mem' := }.carrier
                              theorem AddMonoidHom.eqLocusM.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : M →+ N) :
                              ∀ {a b : M}, f a = g af b = g bf (a + b) = g (a + b)
                              def AddMonoidHom.eqLocusM {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : M →+ N) :

                              The additive submonoid of elements x : M such that f x = g x

                              Equations
                              • f.eqLocusM g = { carrier := {x : M | f x = g x}, add_mem' := , zero_mem' := }
                              Instances For
                                def MonoidHom.eqLocusM {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : M →* N) :

                                The submonoid of elements x : M such that f x = g x

                                Equations
                                • f.eqLocusM g = { carrier := {x : M | f x = g x}, mul_mem' := , one_mem' := }
                                Instances For
                                  @[simp]
                                  theorem AddMonoidHom.eqLocusM_same {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                  f.eqLocusM f =
                                  @[simp]
                                  theorem MonoidHom.eqLocusM_same {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                  f.eqLocusM f =
                                  theorem AddMonoidHom.eqOn_closureM {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {f : M →+ N} {g : M →+ N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) :

                                  If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

                                  theorem MonoidHom.eqOn_closureM {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {f : M →* N} {g : M →* N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) :
                                  Set.EqOn f g (Submonoid.closure s)

                                  If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

                                  theorem AddMonoidHom.eq_of_eqOn_topM {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {f : M →+ N} {g : M →+ N} (h : Set.EqOn f g ) :
                                  f = g
                                  theorem MonoidHom.eq_of_eqOn_topM {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {f : M →* N} {g : M →* N} (h : Set.EqOn f g ) :
                                  f = g
                                  theorem AddMonoidHom.eq_of_eqOn_denseM {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : Set M} (hs : AddSubmonoid.closure s = ) {f : M →+ N} {g : M →+ N} (h : Set.EqOn (⇑f) (⇑g) s) :
                                  f = g
                                  theorem MonoidHom.eq_of_eqOn_denseM {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Set M} (hs : Submonoid.closure s = ) {f : M →* N} {g : M →* N} (h : Set.EqOn (⇑f) (⇑g) s) :
                                  f = g

                                  The additive submonoid consisting of the additive units of an additive monoid

                                  Equations
                                  Instances For
                                    theorem IsAddUnit.addSubmonoid.proof_1 (M : Type u_1) [AddMonoid M] {a : M} {b : M} (ha : a setOf IsAddUnit) (hb : b setOf IsAddUnit) :
                                    a + b setOf IsAddUnit
                                    def IsUnit.submonoid (M : Type u_4) [Monoid M] :

                                    The submonoid consisting of the units of a monoid

                                    Equations
                                    Instances For
                                      def AddMonoidHom.ofClosureMEqTopLeft {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {s : Set M} (f : MN) (hs : AddSubmonoid.closure s = ) (h1 : f 0 = 0) (hmul : xs, ∀ (y : M), f (x + y) = f x + f y) :
                                      M →+ N

                                      Let s be a subset of an additive monoid M such that the closure of s is the whole monoid. Then AddMonoidHom.ofClosureEqTopLeft defines an additive monoid homomorphism from M asking for a proof of f (x + y) = f x + f y only for x ∈ s.

                                      Equations
                                      Instances For
                                        theorem AddMonoidHom.ofClosureMEqTopLeft.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] {s : Set M} (f : MN) (hs : AddSubmonoid.closure s = ) (h1 : f 0 = 0) (hmul : xs, ∀ (y : M), f (x + y) = f x + f y) (x : M) (y : M) :
                                        f (x + y) = f x + f y
                                        def MonoidHom.ofClosureMEqTopLeft {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {s : Set M} (f : MN) (hs : Submonoid.closure s = ) (h1 : f 1 = 1) (hmul : xs, ∀ (y : M), f (x * y) = f x * f y) :
                                        M →* N

                                        Let s be a subset of a monoid M such that the closure of s is the whole monoid. Then MonoidHom.ofClosureEqTopLeft defines a monoid homomorphism from M asking for a proof of f (x * y) = f x * f y only for x ∈ s.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem AddMonoidHom.coe_ofClosureMEqTopLeft {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] {s : Set M} (f : MN) (hs : AddSubmonoid.closure s = ) (h1 : f 0 = 0) (hmul : xs, ∀ (y : M), f (x + y) = f x + f y) :
                                          @[simp]
                                          theorem MonoidHom.coe_ofClosureMEqTopLeft {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {s : Set M} (f : MN) (hs : Submonoid.closure s = ) (h1 : f 1 = 1) (hmul : xs, ∀ (y : M), f (x * y) = f x * f y) :
                                          (MonoidHom.ofClosureMEqTopLeft f hs h1 hmul) = f
                                          def AddMonoidHom.ofClosureMEqTopRight {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {s : Set M} (f : MN) (hs : AddSubmonoid.closure s = ) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
                                          M →+ N

                                          Let s be a subset of an additive monoid M such that the closure of s is the whole monoid. Then AddMonoidHom.ofClosureEqTopRight defines an additive monoid homomorphism from M asking for a proof of f (x + y) = f x + f y only for y ∈ s.

                                          Equations
                                          Instances For
                                            theorem AddMonoidHom.ofClosureMEqTopRight.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] {s : Set M} (f : MN) (hs : AddSubmonoid.closure s = ) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) (x : M) (y : M) :
                                            { toFun := f, map_zero' := h1 }.toFun (x + y) = { toFun := f, map_zero' := h1 }.toFun x + { toFun := f, map_zero' := h1 }.toFun y
                                            def MonoidHom.ofClosureMEqTopRight {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {s : Set M} (f : MN) (hs : Submonoid.closure s = ) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y sf (x * y) = f x * f y) :
                                            M →* N

                                            Let s be a subset of a monoid M such that the closure of s is the whole monoid. Then MonoidHom.ofClosureEqTopRight defines a monoid homomorphism from M asking for a proof of f (x * y) = f x * f y only for y ∈ s.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem AddMonoidHom.coe_ofClosureMEqTopRight {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] {s : Set M} (f : MN) (hs : AddSubmonoid.closure s = ) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
                                              @[simp]
                                              theorem MonoidHom.coe_ofClosureMEqTopRight {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {s : Set M} (f : MN) (hs : Submonoid.closure s = ) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y sf (x * y) = f x * f y) :
                                              (MonoidHom.ofClosureMEqTopRight f hs h1 hmul) = f