# 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 #

• Subsemigroup M: the type of bundled subsemigroup of a magma M; the underlying set is given in the carrier field of the structure, and should be accessed through coercion as in (S : Set M).
• AddSubsemigroup M : the type of bundled subsemigroups of an additive magma M.

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

• Subsemigroup.copy : copy of a subsemigroup with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original Subsemigroup.
• Subsemigroup.closure : semigroup closure of a set, i.e., the least subsemigroup that includes the set.
• Subsemigroup.gi : closure : Set M → Subsemigroup M and coercion coe : Subsemigroup M → Set M form a GaloisInsertion;

## 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} [Mul M] [SetLike S M] [self : ] {s : S} {a : M} {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} [Add M] [SetLike S M] [self : ] {s : S} {a : M} {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 : ) {a : M} {b : M} :
a self.carrierb self.carriera * b self.carrier

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

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 : ) {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 : ) (q : ) (h : p.carrier = q.carrier) :
p = q
Equations
instance Subsemigroup.instSetLike {M : Type u_1} [Mul M] :
SetLike () M
Equations
• Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective' := }
Equations
• =
instance Subsemigroup.instMulMemClass {M : Type u_1} [Mul M] :
Equations
• =
@[simp]
theorem AddSubsemigroup.mem_carrier {M : Type u_1} [Add M] {s : } {x : M} :
x s.carrier x s
@[simp]
theorem Subsemigroup.mem_carrier {M : Type u_1} [Mul M] {s : } {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 : } {T : } (h : ∀ (x : M), x S x T) :
S = T

Two AddSubsemigroups are equal if they have the same elements.

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

Two subsemigroups are equal if they have the same elements.

def AddSubsemigroup.copy {M : Type u_1} [Add M] (S : ) (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
theorem AddSubsemigroup.copy.proof_1 {M : Type u_1} [Add M] (S : ) (s : Set M) (hs : s = S) :
∀ {a b : M}, a sb sa + b s
def Subsemigroup.copy {M : Type u_1} [Mul M] (S : ) (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 : } {s : Set M} (hs : s = S) :
(S.copy s hs) = s
@[simp]
theorem Subsemigroup.coe_copy {M : Type u_1} [Mul M] {S : } {s : Set M} (hs : s = S) :
(S.copy s hs) = s
theorem AddSubsemigroup.copy_eq {M : Type u_1} [Add M] {S : } {s : Set M} (hs : s = S) :
S.copy s hs = S
theorem Subsemigroup.copy_eq {M : Type u_1} [Mul M] {S : } {s : Set M} (hs : s = S) :
S.copy s hs = S
theorem AddSubsemigroup.add_mem {M : Type u_1} [Add M] (S : ) {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 : ) {x : M} {y : M} :
x Sy Sx * y S

A subsemigroup is closed under multiplication.

∀ {a b : M}, a Set.univb Set.univa + b Set.univ

The additive subsemigroup M of the magma M.

Equations
• AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := } }
instance Subsemigroup.instTop {M : Type u_1} [Mul M] :
Top ()

The subsemigroup M of the magma M.

Equations
• Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := } }

The trivial AddSubsemigroup ∅ of an additive magma M.

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

The trivial subsemigroup ∅ of a magma M.

Equations
• Subsemigroup.instBot = { bot := { carrier := , mul_mem' := } }
Equations
• AddSubsemigroup.instInhabited = { default := }
instance Subsemigroup.instInhabited {M : Type u_1} [Mul M] :
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]
= Set.univ
@[simp]
theorem Subsemigroup.coe_top {M : Type u_1} [Mul M] :
= Set.univ
@[simp]
=
@[simp]
theorem Subsemigroup.coe_bot {M : Type u_1} [Mul M] :
=
theorem AddSubsemigroup.instInf.proof_1 {M : Type u_1} [Add M] (S₁ : ) (S₂ : ) :
∀ {a b : M}, a S₁ S₂b S₁ S₂a + b S₁ S₂

The inf of two AddSubsemigroups is their intersection.

Equations
• AddSubsemigroup.instInf = { inf := fun (S₁ S₂ : ) => { carrier := S₁ S₂, add_mem' := } }
abbrev AddSubsemigroup.instInf.match_1 {M : Type u_1} [Add M] (S₁ : ) (S₂ : ) :
∀ {b : M} (motive : b S₁ S₂Prop) (x : b S₁ S₂), (∀ (hy : b S₁) (hy' : b S₂), motive )motive x
Equations
• =
Instances For
instance Subsemigroup.instInf {M : Type u_1} [Mul M] :
Inf ()

The inf of two subsemigroups is their intersection.

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

The AddSubsemigroups of an AddMonoid form a complete lattice.

Equations
• AddSubsemigroup.instCompleteLattice = let __src := ; CompleteLattice.mk
∀ (x x_1 x_2 : ), x x_1x x_2x_3x, x_3 x_1 x_3 x_2
theorem AddSubsemigroup.instCompleteLattice.proof_12 {M : Type u_1} [Add M] (s : ) (a : ) :
a sa sSup s
∀ (x : ), x_1, x_1 x
theorem AddSubsemigroup.instCompleteLattice.proof_14 {M : Type u_1} [Add M] (s : ) (a : ) :
a ssInf s a
∀ (x x_1 : ) (x_2 : M), x_2 x x_2 x_1x_2 x_1
theorem AddSubsemigroup.instCompleteLattice.proof_7 {M : Type u_1} [Add M] (a : ) (b : ) :
b a b
theorem AddSubsemigroup.instCompleteLattice.proof_6 {M : Type u_1} [Add M] (a : ) (b : ) :
a a b
theorem AddSubsemigroup.instCompleteLattice.proof_3 {M : Type u_1} [Add M] (a : ) (b : ) (c : ) :
a bb ca c
∀ (x : ), IsGLB x (sInf x)
instance Subsemigroup.instCompleteLattice {M : Type u_1} [Mul M] :

subsemigroups of a monoid form a complete lattice.

Equations
instance AddSubsemigroup.instNontrivialOfNonempty {M : Type u_1} [Add M] [hn : ] :
Equations
• =
instance Subsemigroup.instNontrivialOfNonempty {M : Type u_1} [Mul M] [hn : ] :
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} :
∀ (S : ), s Sx S
theorem Subsemigroup.mem_closure {M : Type u_1} [Mul M] {s : Set M} {x : M} :
∀ (S : ), s Sx S
@[simp]
theorem AddSubsemigroup.subset_closure {M : Type u_1} [Add M] {s : Set M} :
s

The AddSubsemigroup generated by a set includes the set.

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

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 : ) :
Ps
theorem Subsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [Mul M] {s : Set M} {P : M} (hP : ) :
Ps
@[simp]
theorem AddSubsemigroup.closure_le {M : Type u_1} [Add M] {s : Set M} {S : } :
s S

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 : } :
s S

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 : } (h₁ : s S) (h₂ : ) :
theorem Subsemigroup.closure_eq_of_le {M : Type u_1} [Mul M] {s : Set M} {S : } (h₁ : s S) (h₂ : ) :
theorem AddSubsemigroup.closure_induction {M : Type u_1} [Add M] {s : Set M} {p : MProp} {x : M} (h : ) (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 : ) (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.

abbrev AddSubsemigroup.closure_induction'.match_1 {M : Type u_1} [Add M] (s : Set M) {p : (x : M) → } (y : M) (motive : (∃ (x : ), p y x)Prop) :
∀ (x : ∃ (x : ), p y x), (∀ (hy' : ) (hy : p y hy'), motive )motive x
Equations
• =
Instances For
theorem AddSubsemigroup.closure_induction' {M : Type u_1} [Add M] (s : Set M) {p : (x : M) → } (mem : ∀ (x : M) (h : x s), p x ) (mul : ∀ (x : M) (hx : ) (y : M) (hy : ), p x hxp y hyp (x + y) ) {x : M} (hx : ) :
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) → } (mem : ∀ (x : M) (h : x s), p x ) (mul : ∀ (x : M) (hx : ) (y : M) (hy : ), p x hxp y hyp (x * y) ) {x : M} (hx : ) :
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 : ) (hy : ) (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 : ) (hy : ) (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 : ) (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 : ) (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).

∀ (x : ), x

closure forms a Galois insertion with the coercion to set.

Equations
Instances For
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]
theorem AddSubsemigroup.closure_eq {M : Type u_1} [Add M] (S : ) :

Additive closure of an additive subsemigroup S equals S

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

Closure of a subsemigroup S equals S.

@[simp]
@[simp]
theorem Subsemigroup.closure_empty {M : Type u_1} [Mul M] :
@[simp]
theorem AddSubsemigroup.closure_union {M : Type u_1} [Add M] (s : Set M) (t : Set M) :
theorem Subsemigroup.closure_union {M : Type u_1} [Mul M] (s : Set M) (t : Set M) :
theorem AddSubsemigroup.closure_iUnion {M : Type u_1} [Add M] {ι : Sort u_4} (s : ιSet M) :
AddSubsemigroup.closure (⋃ (i : ι), s i) = ⨆ (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.closure_singleton_le_iff_mem {M : Type u_1} [Add M] (m : M) (p : ) :
m p
theorem Subsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [Mul M] (m : M) (p : ) :
m p
theorem AddSubsemigroup.mem_iSup {M : Type u_1} [Add M] {ι : Sort u_4} (p : ι) {m : M} :
m ⨆ (i : ι), p i ∀ (N : ), (∀ (i : ι), p i N)m N
theorem Subsemigroup.mem_iSup {M : Type u_1} [Mul M] {ι : Sort u_4} (p : ι) {m : M} :
m ⨆ (i : ι), p i ∀ (N : ), (∀ (i : ι), p i N)m N
theorem AddSubsemigroup.iSup_eq_closure {M : Type u_1} [Add M] {ι : Sort u_4} (p : ι) :
⨆ (i : ι), p i = AddSubsemigroup.closure (⋃ (i : ι), (p i))
theorem Subsemigroup.iSup_eq_closure {M : Type u_1} [Mul M] {ι : Sort u_4} (p : ι) :
⨆ (i : ι), p i = Subsemigroup.closure (⋃ (i : ι), (p i))

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
∀ {a b : M}, f a = g af b = g bf (a + b) = g (a + b)
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) :
Set.EqOn f g

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) :
Set.EqOn f g

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 : ) {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 : ) {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn (f) (g) s) :
f = g
theorem AddHom.ofDense.proof_1 {M : Type u_2} {N : Type u_1} [] [] {s : Set M} (f : MN) (hs : ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) (x : M) (y : M) :
f (x + y) = f x + f y
def AddHom.ofDense {M : Type u_4} {N : Type u_5} [] [] {s : Set M} (f : MN) (hs : ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :

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
def MulHom.ofDense {M : Type u_4} {N : Type u_5} [] [] {s : Set M} (f : MN) (hs : ) (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} [] [] {s : Set M} (f : MN) (hs : ) (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} [] [] {s : Set M} (f : MN) (hs : ) (hmul : ∀ (x y : M), y sf (x * y) = f x * f y) :
(MulHom.ofDense f hs hmul) = f