Documentation

Mathlib.Algebra.Group.Subsemigroup.Basic

Subsemigroups: definition and CompleteLattice structure #

This file defines bundled multiplicative and additive subsemigroups. We also define a CompleteLattice structure on Subsemigroups, and define the closure of a set as the minimal subsemigroup that includes this set.

Main definitions #

For each of the following definitions in the Subsemigroup namespace, there is a corresponding definition in the AddSubsemigroup namespace.

Implementation notes #

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

Note that Subsemigroup M does not actually require Semigroup M, instead requiring only the weaker Mul M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

Tags #

subsemigroup, subsemigroups

class MulMemClass (S : Type u_4) (M : Type u_5) [Mul M] [SetLike S M] :

MulMemClass S M says S is a type of sets s : Set M that are closed under (*)

  • mul_mem : ∀ {s : S} {a b : M}, a sb sa * b s

    A substructure satisfying MulMemClass is closed under multiplication.

Instances
    theorem MulMemClass.mul_mem {S : Type u_4} {M : Type u_5} :
    ∀ {inst : Mul M} {inst_1 : SetLike S M} [self : MulMemClass S M] {s : S} {a b : M}, a sb sa * b s

    A substructure satisfying MulMemClass is closed under multiplication.

    class AddMemClass (S : Type u_4) (M : Type u_5) [Add M] [SetLike S M] :

    AddMemClass S M says S is a type of sets s : Set M that are closed under (+)

    • add_mem : ∀ {s : S} {a b : M}, a sb sa + b s

      A substructure satisfying AddMemClass is closed under addition.

    Instances
      theorem AddMemClass.add_mem {S : Type u_4} {M : Type u_5} :
      ∀ {inst : Add M} {inst_1 : SetLike S M} [self : AddMemClass S M] {s : S} {a b : M}, a sb sa + b s

      A substructure satisfying AddMemClass is closed under addition.

      structure Subsemigroup (M : Type u_4) [Mul M] :
      Type u_4

      A subsemigroup of a magma M is a subset closed under multiplication.

      • carrier : Set M

        The carrier of a subsemigroup.

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

        The product of two elements of a subsemigroup belongs to the subsemigroup.

      Instances For
        theorem Subsemigroup.mul_mem' {M : Type u_4} [Mul M] (self : Subsemigroup M) {a : M} {b : M} :
        a self.carrierb self.carriera * b self.carrier

        The product of two elements of a subsemigroup belongs to the subsemigroup.

        structure AddSubsemigroup (M : Type u_4) [Add M] :
        Type u_4

        An additive subsemigroup of an additive magma M is a subset closed under addition.

        • carrier : Set M

          The carrier of an additive subsemigroup.

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

          The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

        Instances For
          theorem AddSubsemigroup.add_mem' {M : Type u_4} [Add M] (self : AddSubsemigroup M) {a : M} {b : M} :
          a self.carrierb self.carriera + b self.carrier

          The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

          theorem AddSubsemigroup.instSetLike.proof_1 {M : Type u_1} [Add M] (p : AddSubsemigroup M) (q : AddSubsemigroup M) (h : p.carrier = q.carrier) :
          p = q
          Equations
          • AddSubsemigroup.instSetLike = { coe := AddSubsemigroup.carrier, coe_injective' := }
          instance Subsemigroup.instSetLike {M : Type u_1} [Mul M] :
          Equations
          • Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective' := }
          Equations
          • =
          Equations
          • =
          @[simp]
          theorem AddSubsemigroup.mem_carrier {M : Type u_1} [Add M] {s : AddSubsemigroup M} {x : M} :
          x s.carrier x s
          @[simp]
          theorem Subsemigroup.mem_carrier {M : Type u_1} [Mul M] {s : Subsemigroup M} {x : M} :
          x s.carrier x s
          @[simp]
          theorem AddSubsemigroup.mem_mk {M : Type u_1} [Add M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a sb sa + b s) :
          x { carrier := s, add_mem' := h_mul } x s
          @[simp]
          theorem Subsemigroup.mem_mk {M : Type u_1} [Mul M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a sb sa * b s) :
          x { carrier := s, mul_mem' := h_mul } x s
          @[simp]
          theorem AddSubsemigroup.coe_set_mk {M : Type u_1} [Add M] (s : Set M) (h_mul : ∀ {a b : M}, a sb sa + b s) :
          { carrier := s, add_mem' := h_mul } = s
          @[simp]
          theorem Subsemigroup.coe_set_mk {M : Type u_1} [Mul M] (s : Set M) (h_mul : ∀ {a b : M}, a sb sa * b s) :
          { carrier := s, mul_mem' := h_mul } = s
          @[simp]
          theorem AddSubsemigroup.mk_le_mk {M : Type u_1} [Add M] {s : Set M} {t : Set M} (h_mul : ∀ {a b : M}, a sb sa + b s) (h_mul' : ∀ {a b : M}, a tb ta + b t) :
          { carrier := s, add_mem' := h_mul } { carrier := t, add_mem' := h_mul' } s t
          @[simp]
          theorem Subsemigroup.mk_le_mk {M : Type u_1} [Mul M] {s : Set M} {t : Set M} (h_mul : ∀ {a b : M}, a sb sa * b s) (h_mul' : ∀ {a b : M}, a tb ta * b t) :
          { carrier := s, mul_mem' := h_mul } { carrier := t, mul_mem' := h_mul' } s t
          theorem AddSubsemigroup.ext {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : ∀ (x : M), x S x T) :
          S = T

          Two AddSubsemigroups are equal if they have the same elements.

          theorem AddSubsemigroup.ext_iff {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} :
          S = T ∀ (x : M), x S x T
          theorem Subsemigroup.ext_iff {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} :
          S = T ∀ (x : M), x S x T
          theorem Subsemigroup.ext {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : ∀ (x : M), x S x T) :
          S = T

          Two subsemigroups are equal if they have the same elements.

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

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

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

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

            Equations
            • S.copy s hs = { carrier := s, mul_mem' := }
            Instances For
              @[simp]
              theorem AddSubsemigroup.coe_copy {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = S) :
              (S.copy s hs) = s
              @[simp]
              theorem Subsemigroup.coe_copy {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = S) :
              (S.copy s hs) = s
              theorem AddSubsemigroup.copy_eq {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = S) :
              S.copy s hs = S
              theorem Subsemigroup.copy_eq {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = S) :
              S.copy s hs = S
              theorem AddSubsemigroup.add_mem {M : Type u_1} [Add M] (S : AddSubsemigroup M) {x : M} {y : M} :
              x Sy Sx + y S

              An AddSubsemigroup is closed under addition.

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

              A subsemigroup is closed under multiplication.

              instance AddSubsemigroup.instTop {M : Type u_1} [Add M] :

              The additive subsemigroup M of the magma M.

              Equations
              • AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := } }
              theorem AddSubsemigroup.instTop.proof_1 {M : Type u_1} [Add M] :
              ∀ {a b : M}, a Set.univb Set.univa + b Set.univ
              instance Subsemigroup.instTop {M : Type u_1} [Mul M] :

              The subsemigroup M of the magma M.

              Equations
              • Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := } }
              instance AddSubsemigroup.instBot {M : Type u_1} [Add M] :

              The trivial AddSubsemigroup of an additive magma M.

              Equations
              • AddSubsemigroup.instBot = { bot := { carrier := , add_mem' := } }
              theorem AddSubsemigroup.instBot.proof_1 {M : Type u_1} [Add M] :
              ∀ {a b : M}, Falseb a + b
              instance Subsemigroup.instBot {M : Type u_1} [Mul M] :

              The trivial subsemigroup of a magma M.

              Equations
              • Subsemigroup.instBot = { bot := { carrier := , mul_mem' := } }
              Equations
              • AddSubsemigroup.instInhabited = { default := }
              Equations
              • Subsemigroup.instInhabited = { default := }
              theorem AddSubsemigroup.not_mem_bot {M : Type u_1} [Add M] {x : M} :
              x
              theorem Subsemigroup.not_mem_bot {M : Type u_1} [Mul M] {x : M} :
              x
              @[simp]
              theorem AddSubsemigroup.mem_top {M : Type u_1} [Add M] (x : M) :
              @[simp]
              theorem Subsemigroup.mem_top {M : Type u_1} [Mul M] (x : M) :
              @[simp]
              theorem AddSubsemigroup.coe_top {M : Type u_1} [Add M] :
              = Set.univ
              @[simp]
              theorem Subsemigroup.coe_top {M : Type u_1} [Mul M] :
              = Set.univ
              @[simp]
              theorem AddSubsemigroup.coe_bot {M : Type u_1} [Add M] :
              =
              @[simp]
              theorem Subsemigroup.coe_bot {M : Type u_1} [Mul M] :
              =
              instance AddSubsemigroup.instInf {M : Type u_1} [Add M] :

              The inf of two AddSubsemigroups is their intersection.

              Equations
              • AddSubsemigroup.instInf = { inf := fun (S₁ S₂ : AddSubsemigroup M) => { carrier := S₁ S₂, add_mem' := } }
              theorem AddSubsemigroup.instInf.proof_1 {M : Type u_1} [Add M] (S₁ : AddSubsemigroup M) (S₂ : AddSubsemigroup M) :
              ∀ {a b : M}, a S₁ S₂b S₁ S₂a + b S₁ S₂
              instance Subsemigroup.instInf {M : Type u_1} [Mul M] :

              The inf of two subsemigroups is their intersection.

              Equations
              • Subsemigroup.instInf = { inf := fun (S₁ S₂ : Subsemigroup M) => { carrier := S₁ S₂, mul_mem' := } }
              @[simp]
              theorem AddSubsemigroup.coe_inf {M : Type u_1} [Add M] (p : AddSubsemigroup M) (p' : AddSubsemigroup M) :
              (p p') = p p'
              @[simp]
              theorem Subsemigroup.coe_inf {M : Type u_1} [Mul M] (p : Subsemigroup M) (p' : Subsemigroup M) :
              (p p') = p p'
              @[simp]
              theorem AddSubsemigroup.mem_inf {M : Type u_1} [Add M] {p : AddSubsemigroup M} {p' : AddSubsemigroup M} {x : M} :
              x p p' x p x p'
              @[simp]
              theorem Subsemigroup.mem_inf {M : Type u_1} [Mul M] {p : Subsemigroup M} {p' : Subsemigroup M} {x : M} :
              x p p' x p x p'
              Equations
              • AddSubsemigroup.instInfSet = { sInf := fun (s : Set (AddSubsemigroup M)) => { carrier := ts, t, add_mem' := } }
              theorem AddSubsemigroup.instInfSet.proof_1 {M : Type u_1} [Add M] (s : Set (AddSubsemigroup M)) :
              ∀ {a b : M}, a ts, tb ts, ta + b xs, x
              instance Subsemigroup.instInfSet {M : Type u_1} [Mul M] :
              Equations
              • Subsemigroup.instInfSet = { sInf := fun (s : Set (Subsemigroup M)) => { carrier := ts, t, mul_mem' := } }
              @[simp]
              theorem AddSubsemigroup.coe_sInf {M : Type u_1} [Add M] (S : Set (AddSubsemigroup M)) :
              (sInf S) = sS, s
              @[simp]
              theorem Subsemigroup.coe_sInf {M : Type u_1} [Mul M] (S : Set (Subsemigroup M)) :
              (sInf S) = sS, s
              theorem AddSubsemigroup.mem_sInf {M : Type u_1} [Add M] {S : Set (AddSubsemigroup M)} {x : M} :
              x sInf S pS, x p
              theorem Subsemigroup.mem_sInf {M : Type u_1} [Mul M] {S : Set (Subsemigroup M)} {x : M} :
              x sInf S pS, x p
              theorem AddSubsemigroup.mem_iInf {M : Type u_1} [Add M] {ι : Sort u_4} {S : ιAddSubsemigroup M} {x : M} :
              x ⨅ (i : ι), S i ∀ (i : ι), x S i
              theorem Subsemigroup.mem_iInf {M : Type u_1} [Mul M] {ι : Sort u_4} {S : ιSubsemigroup M} {x : M} :
              x ⨅ (i : ι), S i ∀ (i : ι), x S i
              @[simp]
              theorem AddSubsemigroup.coe_iInf {M : Type u_1} [Add M] {ι : Sort u_4} {S : ιAddSubsemigroup M} :
              (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
              @[simp]
              theorem Subsemigroup.coe_iInf {M : Type u_1} [Mul M] {ι : Sort u_4} {S : ιSubsemigroup M} :
              (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
              theorem AddSubsemigroup.instCompleteLattice.proof_3 {M : Type u_1} [Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) (c : AddSubsemigroup M) :
              a bb ca c
              theorem AddSubsemigroup.instCompleteLattice.proof_11 {M : Type u_1} [Add M] :
              ∀ (x x_1 x_2 : AddSubsemigroup M), x x_1x x_2x_3x, x_3 x_1 x_3 x_2
              theorem AddSubsemigroup.instCompleteLattice.proof_13 {M : Type u_1} [Add M] (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M) :
              (∀ bs, b a)sSup s a
              theorem AddSubsemigroup.instCompleteLattice.proof_8 {M : Type u_1} [Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) (c : AddSubsemigroup M) :
              a cb ca b c
              theorem AddSubsemigroup.instCompleteLattice.proof_5 {M : Type u_1} [Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) :
              a bb aa = b
              theorem AddSubsemigroup.instCompleteLattice.proof_10 {M : Type u_1} [Add M] :
              ∀ (x x_1 : AddSubsemigroup M) (x_2 : M), x_2 x x_2 x_1x_2 x_1

              The AddSubsemigroups of an AddMonoid form a complete lattice.

              Equations
              theorem AddSubsemigroup.instCompleteLattice.proof_9 {M : Type u_1} [Add M] :
              ∀ (x x_1 : AddSubsemigroup M) (x_2 : M), x_2 x x_2 x_1x_2 x
              theorem AddSubsemigroup.instCompleteLattice.proof_16 {M : Type u_1} [Add M] :
              ∀ (x : AddSubsemigroup M), x_1, x_1 x
              theorem AddSubsemigroup.instCompleteLattice.proof_15 {M : Type u_1} [Add M] (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M) :
              (∀ bs, a b)a sInf s

              subsemigroups of a monoid form a complete lattice.

              Equations
              Equations
              • =
              Equations
              • =
              def AddSubsemigroup.closure {M : Type u_1} [Add M] (s : Set M) :

              The AddSubsemigroup generated by a set

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

                The Subsemigroup generated by a set.

                Equations
                Instances For
                  theorem AddSubsemigroup.mem_closure {M : Type u_1} [Add M] {s : Set M} {x : M} :
                  x AddSubsemigroup.closure s ∀ (S : AddSubsemigroup M), s Sx S
                  theorem Subsemigroup.mem_closure {M : Type u_1} [Mul M] {s : Set M} {x : M} :
                  x Subsemigroup.closure s ∀ (S : Subsemigroup M), s Sx S
                  @[simp]
                  theorem AddSubsemigroup.subset_closure {M : Type u_1} [Add M] {s : Set M} :

                  The AddSubsemigroup generated by a set includes the set.

                  @[simp]
                  theorem Subsemigroup.subset_closure {M : Type u_1} [Mul M] {s : Set M} :

                  The subsemigroup generated by a set includes the set.

                  theorem AddSubsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [Add M] {s : Set M} {P : M} (hP : PAddSubsemigroup.closure s) :
                  Ps
                  theorem Subsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [Mul M] {s : Set M} {P : M} (hP : PSubsemigroup.closure s) :
                  Ps
                  @[simp]
                  theorem AddSubsemigroup.closure_le {M : Type u_1} [Add M] {s : Set M} {S : AddSubsemigroup M} :

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

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

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

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

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

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

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

                  theorem AddSubsemigroup.closure_eq_of_le {M : Type u_1} [Add M] {s : Set M} {S : AddSubsemigroup M} (h₁ : s S) (h₂ : S AddSubsemigroup.closure s) :
                  theorem Subsemigroup.closure_eq_of_le {M : Type u_1} [Mul M] {s : Set M} {S : Subsemigroup M} (h₁ : s S) (h₂ : S Subsemigroup.closure s) :
                  theorem AddSubsemigroup.closure_induction {M : Type u_1} [Add M] {s : Set M} {p : MProp} {x : M} (h : x AddSubsemigroup.closure s) (mem : xs, p x) (mul : ∀ (x y : M), p xp yp (x + y)) :
                  p x

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

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

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

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

                  A dependent version of AddSubsemigroup.closure_induction.

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

                  A dependent version of Subsemigroup.closure_induction.

                  theorem AddSubsemigroup.closure_induction₂ {M : Type u_1} [Add M] {s : Set M} {p : MMProp} {x : M} {y : M} (hx : x AddSubsemigroup.closure s) (hy : y AddSubsemigroup.closure s) (Hs : xs, ys, p x y) (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 Subsemigroup.closure_induction₂ {M : Type u_1} [Mul M] {s : Set M} {p : MMProp} {x : M} {y : M} (hx : x Subsemigroup.closure s) (hy : y Subsemigroup.closure s) (Hs : xs, ys, p x y) (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 AddSubsemigroup.dense_induction {M : Type u_1} [Add M] {p : MProp} (x : M) {s : Set M} (hs : AddSubsemigroup.closure s = ) (mem : xs, p x) (mul : ∀ (x y : M), p xp yp (x + y)) :
                  p x

                  If s is a dense set in an additive monoid M, AddSubsemigroup.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, and verify that p x and p y imply p (x + y).

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

                  If s is a dense set in a magma M, Subsemigroup.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, and verify that p x and p y imply p (x * y).

                  def AddSubsemigroup.gi (M : Type u_1) [Add M] :
                  GaloisInsertion AddSubsemigroup.closure SetLike.coe

                  closure forms a Galois insertion with the coercion to set.

                  Equations
                  Instances For
                    theorem AddSubsemigroup.gi.proof_1 (M : Type u_1) [Add M] :
                    ∀ (x : AddSubsemigroup M), x (AddSubsemigroup.closure x)
                    def Subsemigroup.gi (M : Type u_1) [Mul M] :
                    GaloisInsertion Subsemigroup.closure SetLike.coe

                    closure forms a Galois insertion with the coercion to set.

                    Equations
                    Instances For
                      @[simp]

                      Additive closure of an additive subsemigroup S equals S

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

                      Closure of a subsemigroup S equals S.

                      @[simp]
                      theorem AddSubsemigroup.closure_iUnion {M : Type u_1} [Add M] {ι : Sort u_4} (s : ιSet M) :
                      AddSubsemigroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), AddSubsemigroup.closure (s i)
                      theorem Subsemigroup.closure_iUnion {M : Type u_1} [Mul M] {ι : Sort u_4} (s : ιSet M) :
                      Subsemigroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Subsemigroup.closure (s i)
                      theorem AddSubsemigroup.mem_iSup {M : Type u_1} [Add M] {ι : Sort u_4} (p : ιAddSubsemigroup M) {m : M} :
                      m ⨆ (i : ι), p i ∀ (N : AddSubsemigroup M), (∀ (i : ι), p i N)m N
                      theorem Subsemigroup.mem_iSup {M : Type u_1} [Mul M] {ι : Sort u_4} (p : ιSubsemigroup M) {m : M} :
                      m ⨆ (i : ι), p i ∀ (N : Subsemigroup M), (∀ (i : ι), p i N)m N
                      theorem AddSubsemigroup.iSup_eq_closure {M : Type u_1} [Add M] {ι : Sort u_4} (p : ιAddSubsemigroup M) :
                      ⨆ (i : ι), p i = AddSubsemigroup.closure (⋃ (i : ι), (p i))
                      theorem Subsemigroup.iSup_eq_closure {M : Type u_1} [Mul M] {ι : Sort u_4} (p : ιSubsemigroup M) :
                      ⨆ (i : ι), p i = Subsemigroup.closure (⋃ (i : ι), (p i))
                      theorem AddHom.eqLocus.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (g : AddHom M N) :
                      ∀ {a b : M}, f a = g af b = g bf (a + b) = g (a + b)
                      def AddHom.eqLocus {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : AddHom M N) :

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

                      Equations
                      • f.eqLocus g = { carrier := {x : M | f x = g x}, add_mem' := }
                      Instances For
                        def MulHom.eqLocus {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (g : M →ₙ* N) :

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

                        Equations
                        • f.eqLocus g = { carrier := {x : M | f x = g x}, mul_mem' := }
                        Instances For
                          theorem AddHom.eqOn_closure {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {g : AddHom M N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) :

                          If two add homomorphisms are equal on a set, then they are equal on its additive subsemigroup closure.

                          theorem MulHom.eqOn_closure {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {g : M →ₙ* N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) :

                          If two mul homomorphisms are equal on a set, then they are equal on its subsemigroup closure.

                          theorem AddHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {g : AddHom M N} (h : Set.EqOn f g ) :
                          f = g
                          theorem MulHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn f g ) :
                          f = g
                          theorem AddHom.eq_of_eqOn_dense {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : Set M} (hs : AddSubsemigroup.closure s = ) {f : AddHom M N} {g : AddHom M N} (h : Set.EqOn (⇑f) (⇑g) s) :
                          f = g
                          theorem MulHom.eq_of_eqOn_dense {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : Set M} (hs : Subsemigroup.closure s = ) {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn (⇑f) (⇑g) s) :
                          f = g
                          def AddHom.ofDense {M : Type u_4} {N : Type u_5} [AddSemigroup M] [AddSemigroup N] {s : Set M} (f : MN) (hs : AddSubsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
                          AddHom M N

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

                          Equations
                          Instances For
                            theorem AddHom.ofDense.proof_1 {M : Type u_2} {N : Type u_1} [AddSemigroup M] [AddSemigroup N] {s : Set M} (f : MN) (hs : AddSubsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) (x : M) (y : M) :
                            f (x + y) = f x + f y
                            def MulHom.ofDense {M : Type u_4} {N : Type u_5} [Semigroup M] [Semigroup N] {s : Set M} (f : MN) (hs : Subsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x * y) = f x * f y) :

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

                            Equations
                            Instances For
                              @[simp]
                              theorem AddHom.coe_ofDense {M : Type u_1} {N : Type u_2} [AddSemigroup M] [AddSemigroup N] {s : Set M} (f : MN) (hs : AddSubsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
                              (AddHom.ofDense f hs hmul) = f
                              @[simp]
                              theorem MulHom.coe_ofDense {M : Type u_1} {N : Type u_2} [Semigroup M] [Semigroup N] {s : Set M} (f : MN) (hs : Subsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x * y) = f x * f y) :
                              (MulHom.ofDense f hs hmul) = f