# Operations on Submonoids #

In this file we define various operations on Submonoids and MonoidHoms.

## Main definitions #

### Conversion between multiplicative and additive definitions #

• Submonoid.toAddSubmonoid, Submonoid.toAddSubmonoid', AddSubmonoid.toSubmonoid, AddSubmonoid.toSubmonoid': convert between multiplicative and additive submonoids of M, Multiplicative M, and Additive M. These are stated as OrderIsos.

### (Commutative) monoid structure on a submonoid #

• Submonoid.toMonoid, Submonoid.toCommMonoid: a submonoid inherits a (commutative) monoid structure.

### Group actions by submonoids #

• Submonoid.MulAction, Submonoid.DistribMulAction: a submonoid inherits (distributive) multiplicative actions.

### Operations on submonoids #

• Submonoid.comap: preimage of a submonoid under a monoid homomorphism as a submonoid of the domain;
• Submonoid.map: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;
• Submonoid.prod: product of two submonoids s : Submonoid M and t : Submonoid N as a submonoid of M × N;

### Monoid homomorphisms between submonoid #

• Submonoid.subtype: embedding of a submonoid into the ambient monoid.
• Submonoid.inclusion: given two submonoids S, T such that S ≤ T, S.inclusion T is the inclusion of S into T as a monoid homomorphism;
• MulEquiv.submonoidCongr: converts a proof of S = T into a monoid isomorphism between S and T.
• Submonoid.prodEquiv: monoid isomorphism between s.prod t and s × t;

### Operations on MonoidHoms #

• MonoidHom.mrange: range of a monoid homomorphism as a submonoid of the codomain;
• MonoidHom.mker: kernel of a monoid homomorphism as a submonoid of the domain;
• MonoidHom.restrict: restrict a monoid homomorphism to a submonoid;
• MonoidHom.codRestrict: restrict the codomain of a monoid homomorphism to a submonoid;
• MonoidHom.mrangeRestrict: restrict a monoid homomorphism to its range;

## Tags #

submonoid, range, product, map, comap

### Conversion to/from Additive/Multiplicative#

@[simp]
theorem Submonoid.toAddSubmonoid_symm_apply_coe {M : Type u_1} [] (S : ) :
@[simp]
theorem Submonoid.toAddSubmonoid_apply_coe {M : Type u_1} [] (S : ) :
def Submonoid.toAddSubmonoid {M : Type u_1} [] :

Submonoids of monoid M are isomorphic to additive submonoids of Additive M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]
abbrev AddSubmonoid.toSubmonoid' {M : Type u_1} [] :

Additive submonoids of an additive monoid Additive M are isomorphic to submonoids of M.

Equations
Instances For
theorem Submonoid.toAddSubmonoid_closure {M : Type u_1} [] (S : Set M) :
theorem AddSubmonoid.toSubmonoid'_closure {M : Type u_1} [] (S : Set ()) :
@[simp]
theorem AddSubmonoid.toSubmonoid_apply_coe {A : Type u_4} [] (S : ) :
@[simp]
theorem AddSubmonoid.toSubmonoid_symm_apply_coe {A : Type u_4} [] (S : ) :
def AddSubmonoid.toSubmonoid {A : Type u_4} [] :

Additive submonoids of an additive monoid A are isomorphic to multiplicative submonoids of Multiplicative A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]
abbrev Submonoid.toAddSubmonoid' {A : Type u_4} [] :

Submonoids of a monoid Multiplicative A are isomorphic to additive submonoids of A.

Equations
Instances For
theorem AddSubmonoid.toSubmonoid_closure {A : Type u_4} [] (S : Set A) :
theorem Submonoid.toAddSubmonoid'_closure {A : Type u_4} [] (S : ) :

### comap and map#

theorem AddSubmonoid.comap.proof_2 {M : Type u_2} {N : Type u_1} [] [] {F : Type u_3} [FunLike F M N] [mc : ] (f : F) (S : ) :
f 0 S
theorem AddSubmonoid.comap.proof_1 {M : Type u_1} {N : Type u_2} [] [] {F : Type u_3} [FunLike F M N] [mc : ] (f : F) (S : ) :
∀ {a b : M}, a f ⁻¹' Sb f ⁻¹' Sf (a + b) S
def AddSubmonoid.comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) :

The preimage of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

Equations
• = { toAddSubsemigroup := { carrier := f ⁻¹' S, add_mem' := }, zero_mem' := }
Instances For
def Submonoid.comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) :

The preimage of a submonoid along a monoid homomorphism is a submonoid.

Equations
• = { toSubsemigroup := { carrier := f ⁻¹' S, mul_mem' := }, one_mem' := }
Instances For
@[simp]
theorem AddSubmonoid.coe_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (S : ) (f : F) :
() = f ⁻¹' S
@[simp]
theorem Submonoid.coe_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (S : ) (f : F) :
() = f ⁻¹' S
@[simp]
theorem AddSubmonoid.mem_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {S : } {f : F} {x : M} :
x f x S
@[simp]
theorem Submonoid.mem_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {S : } {f : F} {x : M} :
x f x S
theorem AddSubmonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (S : ) (g : N →+ P) (f : M →+ N) :
=
theorem Submonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (S : ) (g : N →* P) (f : M →* N) :
=
@[simp]
theorem AddSubmonoid.comap_id {P : Type u_3} [] (S : ) :
@[simp]
theorem Submonoid.comap_id {P : Type u_3} [] (S : ) :
= S
theorem AddSubmonoid.map.proof_1 {M : Type u_2} {N : Type u_1} [] [] {F : Type u_3} [FunLike F M N] [mc : ] (f : F) (S : ) :
∀ {a b : N}, a f '' Sb f '' Sa + b f '' S
def AddSubmonoid.map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) :

The image of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

Equations
• = { toAddSubsemigroup := { carrier := f '' S, add_mem' := }, zero_mem' := }
Instances For
theorem AddSubmonoid.map.proof_2 {M : Type u_1} {N : Type u_2} [] [] {F : Type u_3} [FunLike F M N] [mc : ] (f : F) (S : ) :
∃ a ∈ S, f a = 0
def Submonoid.map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) :

The image of a submonoid along a monoid homomorphism is a submonoid.

Equations
• = { toSubsemigroup := { carrier := f '' S, mul_mem' := }, one_mem' := }
Instances For
@[simp]
theorem AddSubmonoid.coe_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) :
() = f '' S
@[simp]
theorem Submonoid.coe_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) :
() = f '' S
@[simp]
theorem AddSubmonoid.mem_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} {S : } {y : N} :
y ∃ x ∈ S, f x = y
@[simp]
theorem Submonoid.mem_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} {S : } {y : N} :
y ∃ x ∈ S, f x = y
theorem AddSubmonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) {S : } {x : M} (hx : x S) :
f x
theorem Submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) {S : } {x : M} (hx : x S) :
f x
theorem AddSubmonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) (x : S) :
f x
theorem Submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) (S : ) (x : S) :
f x
theorem AddSubmonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (S : ) (g : N →+ P) (f : M →+ N) :
=
theorem Submonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (S : ) (g : N →* P) (f : M →* N) :
@[simp]
theorem AddSubmonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) {S : } {x : M} :
f x x S
@[simp]
theorem Submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) {S : } {x : M} :
f x x S
theorem AddSubmonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} {S : } {T : } :
T S
theorem Submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} {S : } {T : } :
T S
theorem AddSubmonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) :
theorem Submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) :
theorem AddSubmonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {T : } {f : F} :
S T
theorem Submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {T : } {f : F} :
S T
theorem AddSubmonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {T : } {f : F} :
TS
theorem Submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {T : } {f : F} :
TS
theorem AddSubmonoid.le_comap_map {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
S
theorem Submonoid.le_comap_map {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
theorem AddSubmonoid.map_comap_le {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {S : } {f : F} :
S
theorem Submonoid.map_comap_le {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {S : } {f : F} :
theorem AddSubmonoid.monotone_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
theorem Submonoid.monotone_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
theorem AddSubmonoid.monotone_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
theorem Submonoid.monotone_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
@[simp]
theorem AddSubmonoid.map_comap_map {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
=
@[simp]
theorem Submonoid.map_comap_map {M : Type u_1} {N : Type u_2} [] [] (S : ) {F : Type u_4} [FunLike F M N] [mc : ] {f : F} :
@[simp]
theorem AddSubmonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {S : } {f : F} :
=
@[simp]
theorem Submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {S : } {f : F} :
theorem AddSubmonoid.map_sup {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (S : ) (T : ) (f : F) :
theorem Submonoid.map_sup {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (S : ) (T : ) (f : F) :
theorem AddSubmonoid.map_iSup {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Sort u_5} (f : F) (s : ι) :
AddSubmonoid.map f (iSup s) = ⨆ (i : ι), AddSubmonoid.map f (s i)
theorem Submonoid.map_iSup {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Sort u_5} (f : F) (s : ι) :
Submonoid.map f (iSup s) = ⨆ (i : ι), Submonoid.map f (s i)
theorem AddSubmonoid.comap_inf {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (S : ) (T : ) (f : F) :
theorem Submonoid.comap_inf {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (S : ) (T : ) (f : F) :
theorem AddSubmonoid.comap_iInf {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Sort u_5} (f : F) (s : ι) :
= ⨅ (i : ι), AddSubmonoid.comap f (s i)
theorem Submonoid.comap_iInf {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Sort u_5} (f : F) (s : ι) :
Submonoid.comap f (iInf s) = ⨅ (i : ι), Submonoid.comap f (s i)
@[simp]
theorem AddSubmonoid.map_bot {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) :
@[simp]
theorem Submonoid.map_bot {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) :
@[simp]
theorem AddSubmonoid.comap_top {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) :
@[simp]
theorem Submonoid.comap_top {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] (f : F) :
abbrev AddSubmonoid.map_id.match_1 {M : Type u_1} [] (S : ) :
∀ (x : M) (motive : x Prop) (x_1 : x ), (∀ (h : x S), motive )motive x_1
Equations
• =
Instances For
@[simp]
theorem AddSubmonoid.map_id {M : Type u_1} [] (S : ) :
= S
@[simp]
theorem Submonoid.map_id {M : Type u_1} [] (S : ) :
= S
theorem AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_3} [] [] {F : Type u_2} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (x : M) :
x x S
def AddSubmonoid.gciMapComap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :

map f and comap f form a GaloisCoinsertion when f is injective.

Equations
Instances For
def Submonoid.gciMapComap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :

map f and comap f form a GaloisCoinsertion when f is injective.

Equations
Instances For
theorem AddSubmonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) :
= S
theorem Submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) :
theorem AddSubmonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem Submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem AddSubmonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem Submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem AddSubmonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
theorem Submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
theorem AddSubmonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
AddSubmonoid.comap f (⨅ (i : ι), AddSubmonoid.map f (S i)) = iInf S
theorem Submonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
Submonoid.comap f (⨅ (i : ι), Submonoid.map f (S i)) = iInf S
theorem AddSubmonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
theorem Submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
theorem AddSubmonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
AddSubmonoid.comap f (⨆ (i : ι), AddSubmonoid.map f (S i)) = iSup S
theorem Submonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
Submonoid.comap f (⨆ (i : ι), Submonoid.map f (S i)) = iSup S
theorem AddSubmonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) {S : } {T : } :
S T
theorem Submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) {S : } {T : } :
S T
theorem AddSubmonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem Submonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
abbrev AddSubmonoid.giMapComap.match_1 {M : Type u_1} {N : Type u_2} {F : Type u_3} [FunLike F M N] {f : F} (x : N) (motive : (∃ (a : M), f a = x)Prop) :
∀ (x_1 : ∃ (a : M), f a = x), (∀ (y : M) (hy : f y = x), motive )motive x_1
Equations
• =
Instances For
def AddSubmonoid.giMapComap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :

map f and comap f form a GaloisInsertion when f is surjective.

Equations
Instances For
theorem AddSubmonoid.giMapComap.proof_1 {M : Type u_3} {N : Type u_1} [] [] {F : Type u_2} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (x : N) (h : x S) :
x
def Submonoid.giMapComap {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :

map f and comap f form a GaloisInsertion when f is surjective.

Equations
Instances For
theorem AddSubmonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) :
= S
theorem Submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) :
theorem AddSubmonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem Submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem AddSubmonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem Submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem AddSubmonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
= S T
theorem Submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
theorem AddSubmonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
AddSubmonoid.map f (⨅ (i : ι), AddSubmonoid.comap f (S i)) = iInf S
theorem Submonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
Submonoid.map f (⨅ (i : ι), Submonoid.comap f (S i)) = iInf S
theorem AddSubmonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
= S T
theorem Submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (T : ) :
theorem AddSubmonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
AddSubmonoid.map f (⨆ (i : ι), AddSubmonoid.comap f (S i)) = iSup S
theorem Submonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {ι : Type u_5} {f : F} (hf : ) (S : ι) :
Submonoid.map f (⨆ (i : ι), Submonoid.comap f (S i)) = iSup S
theorem AddSubmonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) {S : } {T : } :
S T
theorem Submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) {S : } {T : } :
S T
theorem AddSubmonoid.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
theorem Submonoid.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_4} [FunLike F M N] [mc : ] {f : F} (hf : ) :
instance ZeroMemClass.zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :
Zero S'

An AddSubmonoid of an AddMonoid inherits a zero.

Equations
• = { zero := { val := 0, property := } }
instance OneMemClass.one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
One S'

A submonoid of a monoid inherits a 1.

Equations
• = { one := { val := 1, property := } }
@[simp]
theorem ZeroMemClass.coe_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :
0 = 0
@[simp]
theorem OneMemClass.coe_one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
1 = 1
@[simp]
theorem ZeroMemClass.coe_eq_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] {S' : A} {x : S'} :
x = 0 x = 0
@[simp]
theorem OneMemClass.coe_eq_one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] {S' : A} {x : S'} :
x = 1 x = 1
theorem ZeroMemClass.zero_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :
0 = { val := 0, property := }
theorem OneMemClass.one_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
1 = { val := 1, property := }
instance AddSubmonoidClass.nSMul {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] (S : A) :
SMul S

An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

Equations
• = { smul := fun (n : ) (a : S) => { val := n a, property := } }
instance SubmonoidClass.nPow {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] (S : A) :
Pow S

A submonoid of a monoid inherits a power operator.

Equations
• = { pow := fun (a : S) (n : ) => { val := a ^ n, property := } }
@[simp]
theorem AddSubmonoidClass.coe_nsmul {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] {S : A} (x : S) (n : ) :
(n x) = n x
@[simp]
theorem SubmonoidClass.coe_pow {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] {S : A} (x : S) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem AddSubmonoidClass.mk_nsmul {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] {S : A} (x : M) (hx : x S) (n : ) :
n { val := x, property := hx } = { val := n x, property := }
@[simp]
theorem SubmonoidClass.mk_pow {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] {S : A} (x : M) (hx : x S) (n : ) :
{ val := x, property := hx } ^ n = { val := x ^ n, property := }
theorem AddSubmonoidClass.toAddZeroClass.proof_3 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
theorem AddSubmonoidClass.toAddZeroClass.proof_2 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
0 = 0
instance AddSubmonoidClass.toAddZeroClass {M : Type u_5} [] {A : Type u_6} [SetLike A M] [] (S : A) :

An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

Equations
theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
Function.Injective fun (a : S) => a
instance SubmonoidClass.toMulOneClass {M : Type u_5} [] {A : Type u_6} [SetLike A M] [] (S : A) :

A submonoid of a unital magma inherits a unital magma structure.

Equations
theorem AddSubmonoidClass.toAddMonoid.proof_4 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
instance AddSubmonoidClass.toAddMonoid {M : Type u_5} [] {A : Type u_6} [SetLike A M] [] (S : A) :

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations
theorem AddSubmonoidClass.toAddMonoid.proof_1 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] :
theorem AddSubmonoidClass.toAddMonoid.proof_3 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
0 = 0
theorem AddSubmonoidClass.toAddMonoid.proof_5 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
Function.Injective fun (a : S) => a
instance SubmonoidClass.toMonoid {M : Type u_5} [] {A : Type u_6} [SetLike A M] [] (S : A) :
Monoid S

A submonoid of a monoid inherits a monoid structure.

Equations
theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
Function.Injective fun (a : S) => a
theorem AddSubmonoidClass.toAddCommMonoid.proof_5 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
instance AddSubmonoidClass.toAddCommMonoid {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] (S : A) :

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations
theorem AddSubmonoidClass.toAddCommMonoid.proof_3 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
0 = 0
theorem AddSubmonoidClass.toAddCommMonoid.proof_1 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] :
theorem AddSubmonoidClass.toAddCommMonoid.proof_4 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
instance SubmonoidClass.toCommMonoid {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] (S : A) :

A submonoid of a CommMonoid is a CommMonoid.

Equations
theorem AddSubmonoidClass.subtype.proof_1 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [hA : ] (S' : A) :
0 = 0
theorem AddSubmonoidClass.subtype.proof_2 {M : Type u_1} [] {A : Type u_2} [SetLike A M] (S' : A) :
∀ (x x_1 : S'), x + x_1 = x + x_1
def AddSubmonoidClass.subtype {M : Type u_1} [] {A : Type u_4} [SetLike A M] [hA : ] (S' : A) :
S' →+ M

The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

Equations
• = { toZeroHom := { toFun := Subtype.val, map_zero' := }, map_add' := }
Instances For
def SubmonoidClass.subtype {M : Type u_1} [] {A : Type u_4} [SetLike A M] [hA : ] (S' : A) :
S' →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations
• = { toOneHom := { toFun := Subtype.val, map_one' := }, map_mul' := }
Instances For
@[simp]
theorem AddSubmonoidClass.coe_subtype {M : Type u_1} [] {A : Type u_4} [SetLike A M] [hA : ] (S' : A) :
= Subtype.val
@[simp]
theorem SubmonoidClass.coe_subtype {M : Type u_1} [] {A : Type u_4} [SetLike A M] [hA : ] (S' : A) :
= Subtype.val
theorem AddSubmonoid.add.proof_1 {M : Type u_1} [] (S : ) (a : S) (b : S) :
a + b S

An AddSubmonoid of an AddMonoid inherits an addition.

Equations
• = { add := fun (a b : S) => { val := a + b, property := } }
instance Submonoid.mul {M : Type u_1} [] (S : ) :
Mul S

A submonoid of a monoid inherits a multiplication.

Equations
• = { mul := fun (a b : S) => { val := a * b, property := } }
instance AddSubmonoid.zero {M : Type u_1} [] (S : ) :
Zero S

An AddSubmonoid of an AddMonoid inherits a zero.

Equations
• = { zero := { val := 0, property := } }
instance Submonoid.one {M : Type u_1} [] (S : ) :
One S

A submonoid of a monoid inherits a 1.

Equations
• = { one := { val := 1, property := } }
@[simp]
theorem AddSubmonoid.coe_add {M : Type u_1} [] (S : ) (x : S) (y : S) :
(x + y) = x + y
@[simp]
theorem Submonoid.coe_mul {M : Type u_1} [] (S : ) (x : S) (y : S) :
(x * y) = x * y
@[simp]
theorem AddSubmonoid.coe_zero {M : Type u_1} [] (S : ) :
0 = 0
@[simp]
theorem Submonoid.coe_one {M : Type u_1} [] (S : ) :
1 = 1
@[simp]
theorem AddSubmonoid.mk_eq_zero {M : Type u_1} [] (S : ) {a : M} {ha : a S} :
{ val := a, property := ha } = 0 a = 0
@[simp]
theorem Submonoid.mk_eq_one {M : Type u_1} [] (S : ) {a : M} {ha : a S} :
{ val := a, property := ha } = 1 a = 1
@[simp]
theorem AddSubmonoid.mk_add_mk {M : Type u_1} [] (S : ) (x : M) (y : M) (hx : x S) (hy : y S) :
{ val := x, property := hx } + { val := y, property := hy } = { val := x + y, property := }
@[simp]
theorem Submonoid.mk_mul_mk {M : Type u_1} [] (S : ) (x : M) (y : M) (hx : x S) (hy : y S) :
{ val := x, property := hx } * { val := y, property := hy } = { val := x * y, property := }
theorem AddSubmonoid.add_def {M : Type u_1} [] (S : ) (x : S) (y : S) :
x + y = { val := x + y, property := }
theorem Submonoid.mul_def {M : Type u_1} [] (S : ) (x : S) (y : S) :
x * y = { val := x * y, property := }
theorem AddSubmonoid.zero_def {M : Type u_1} [] (S : ) :
0 = { val := 0, property := }
theorem Submonoid.one_def {M : Type u_1} [] (S : ) :
1 = { val := 1, property := }
Function.Injective fun (a : S) => a
0 = 0
∀ (x x_1 : S), (x + x_1) = (x + x_1)

An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

Equations
instance Submonoid.toMulOneClass {M : Type u_5} [] (S : ) :

A submonoid of a unital magma inherits a unital magma structure.

Equations
theorem AddSubmonoid.nsmul_mem {M : Type u_5} [] (S : ) {x : M} (hx : x S) (n : ) :
n x S
theorem Submonoid.pow_mem {M : Type u_5} [] (S : ) {x : M} (hx : x S) (n : ) :
x ^ n S
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
0 = 0
∀ (x x_1 : S), (x + x_1) = (x + x_1)
Function.Injective fun (a : S) => a

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations
instance Submonoid.toMonoid {M : Type u_5} [] (S : ) :
Monoid S

A submonoid of a monoid inherits a monoid structure.

Equations
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations
∀ (x x_1 : S), (x + x_1) = (x + x_1)
Function.Injective fun (a : S) => a
0 = 0
instance Submonoid.toCommMonoid {M : Type u_5} [] (S : ) :

A submonoid of a CommMonoid is a CommMonoid.

Equations
def AddSubmonoid.subtype {M : Type u_1} [] (S : ) :
S →+ M

The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

Equations
• = { toZeroHom := { toFun := Subtype.val, map_zero' := }, map_add' := }
Instances For
theorem AddSubmonoid.subtype.proof_1 {M : Type u_1} [] (S : ) :
0 = 0
theorem AddSubmonoid.subtype.proof_2 {M : Type u_1} [] (S : ) :
∀ (x x_1 : S), x + x_1 = x + x_1
def Submonoid.subtype {M : Type u_1} [] (S : ) :
S →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations
• = { toOneHom := { toFun := Subtype.val, map_one' := }, map_mul' := }
Instances For
@[simp]
theorem AddSubmonoid.coe_subtype {M : Type u_1} [] (S : ) :
= Subtype.val
@[simp]
theorem Submonoid.coe_subtype {M : Type u_1} [] (S : ) :
= Subtype.val
def AddSubmonoid.topEquiv {M : Type u_1} [] :
≃+ M

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [] (x : ) :
{ val := x, property := } = x
theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [] :
∀ (x : M), (fun (x : ) => x) ((fun (x : M) => { val := x, property := }) x) = (fun (x : ) => x) ((fun (x : M) => { val := x, property := }) x)
theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [] :
∀ (x x_1 : ), { toFun := fun (x : ) => x, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : ) => x, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }.toFun (x + x_1)
@[simp]
theorem AddSubmonoid.topEquiv_apply {M : Type u_1} [] (x : ) :
@[simp]
theorem Submonoid.topEquiv_symm_apply_coe {M : Type u_1} [] (x : M) :
((MulEquiv.symm Submonoid.topEquiv) x) = x
@[simp]
theorem Submonoid.topEquiv_apply {M : Type u_1} [] (x : ) :
Submonoid.topEquiv x = x
@[simp]
theorem AddSubmonoid.topEquiv_symm_apply_coe {M : Type u_1} [] (x : M) :
def Submonoid.topEquiv {M : Type u_1} [] :
≃* M

The top submonoid is isomorphic to the monoid.

Equations
• Submonoid.topEquiv = { toEquiv := { toFun := fun (x : ) => x, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }, map_mul' := }
Instances For
@[simp]
@[simp]
theorem Submonoid.topEquiv_toMonoidHom {M : Type u_1} [] :
MulEquiv.toMonoidHom Submonoid.topEquiv =
theorem AddSubmonoid.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) (hf : ) :
∀ (x x_1 : S), (Equiv.Set.image (f) (S) hf).toFun (x + x_1) = (Equiv.Set.image (f) (S) hf).toFun x + (Equiv.Set.image (f) (S) hf).toFun x_1
noncomputable def AddSubmonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) (hf : ) :
S ≃+ ()

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubmonoidMap for better definitional equalities.

Equations
• = let __src := Equiv.Set.image (f) (S) hf; { toEquiv := __src, map_add' := }
Instances For
noncomputable def Submonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →* N) (hf : ) :
S ≃* ()

A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use MulEquiv.submonoidMap for better definitional equalities.

Equations
• = let __src := Equiv.Set.image (f) (S) hf; { toEquiv := __src, map_mul' := }
Instances For
@[simp]
theorem AddSubmonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) (hf : ) (x : S) :
(() x) = f x
@[simp]
theorem Submonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →* N) (hf : ) (x : S) :
(() x) = f x
@[simp]
theorem AddSubmonoid.closure_closure_coe_preimage {M : Type u_1} [] {s : Set M} :
@[simp]
theorem Submonoid.closure_closure_coe_preimage {M : Type u_1} [] {s : Set M} :
Submonoid.closure (Subtype.val ⁻¹' s) =
theorem AddSubmonoid.prod.proof_2 {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
0.1 s 0.2 t
theorem AddSubmonoid.prod.proof_1 {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
∀ {a b : M × N}, a s ×ˢ tb s ×ˢ t(a + b).1 s (a + b).2 t
def AddSubmonoid.prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :

Given AddSubmonoids s, t of AddMonoids A, B respectively, s × t as an AddSubmonoid of A × B.

Equations
• = { toAddSubsemigroup := { carrier := s ×ˢ t, add_mem' := }, zero_mem' := }
Instances For
def Submonoid.prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :

Given submonoids s, t of monoids M, N respectively, s × t as a submonoid of M × N.

Equations
• = { toSubsemigroup := { carrier := s ×ˢ t, mul_mem' := }, one_mem' := }
Instances For
theorem AddSubmonoid.coe_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
() = s ×ˢ t
theorem Submonoid.coe_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
() = s ×ˢ t
theorem AddSubmonoid.mem_prod {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {p : M × N} :
p p.1 s p.2 t
theorem Submonoid.mem_prod {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {p : M × N} :
p p.1 s p.2 t
theorem AddSubmonoid.prod_mono {M : Type u_1} {N : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
theorem Submonoid.prod_mono {M : Type u_1} {N : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
Submonoid.prod s₁ t₁ Submonoid.prod s₂ t₂
theorem AddSubmonoid.prod_top {M : Type u_1} {N : Type u_2} [] [] (s : ) :
theorem Submonoid.prod_top {M : Type u_1} {N : Type u_2} [] [] (s : ) :
theorem AddSubmonoid.top_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) :
theorem Submonoid.top_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) :
@[simp]
theorem AddSubmonoid.top_prod_top {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [] [] :
theorem AddSubmonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [] [] :
theorem Submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [] [] :
def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
() ≃+ s × t

The product of additive submonoids is isomorphic to their product as additive monoids

Equations
• = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_add' := }
Instances For
theorem AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
∀ (x x_1 : ()), (Equiv.Set.prod s t).toFun (x + x_1) = (Equiv.Set.prod s t).toFun (x + x_1)
def Submonoid.prodEquiv {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
() ≃* s × t

The product of submonoids is isomorphic to their product as monoids.

Equations
• = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_mul' := }
Instances For
abbrev AddSubmonoid.map_inl.match_2 {M : Type u_1} {N : Type u_2} [] [] (s : ) (p : M × N) (motive : Prop) :
∀ (x : ), (∀ (hps : p.1 s) (hp1 : p.2 ), motive )motive x
Equations
• =
Instances For
abbrev AddSubmonoid.map_inl.match_1 {M : Type u_1} {N : Type u_2} [] [] (s : ) (p : M × N) (motive : p Prop) :
∀ (x : p ), (∀ (w : M) (hx : w s) (hp : () w = p), motive )motive x
Equations
• =
Instances For
theorem AddSubmonoid.map_inl {M : Type u_1} {N : Type u_2} [] [] (s : ) :
theorem Submonoid.map_inl {M : Type u_1} {N : Type u_2} [] [] (s : ) :
abbrev AddSubmonoid.map_inr.match_1 {M : Type u_1} {N : Type u_2} [] [] (s : ) (p : M × N) (motive : p Prop) :
∀ (x : p ), (∀ (w : N) (hx : w s) (hp : () w = p), motive )motive x
Equations
• =
Instances For
theorem AddSubmonoid.map_inr {M : Type u_1} {N : Type u_2} [] [] (s : ) :
abbrev AddSubmonoid.map_inr.match_2 {M : Type u_1} {N : Type u_2} [] [] (s : ) (p : M × N) (motive : Prop) :
∀ (x : ), (∀ (hp1 : p.1 ) (hps : p.2 s), motive )motive x
Equations
• =
Instances For
theorem Submonoid.map_inr {M : Type u_1} {N : Type u_2} [] [] (s : ) :
@[simp]
theorem AddSubmonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
@[simp]
theorem Submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
=
theorem AddSubmonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [] [] {f : M ≃+ N} {K : } {x : N} :
() x K
theorem Submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [] [] {f : M ≃* N} {K : } {x : N} :
() x K
theorem AddSubmonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [] [] (f : M ≃+ N) (K : ) :
theorem Submonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [] [] (f : M ≃* N) (K : ) :
theorem AddSubmonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [] [] (f : N ≃+ M) (K : ) :
theorem Submonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [] [] (f : N ≃* M) (K : ) :
@[simp]
theorem AddSubmonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [] [] (f : M ≃+ N) :
@[simp]
theorem Submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [] [] (f : M ≃* N) :
theorem AddSubmonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {u : AddSubmonoid (M × N)} :
u s t
theorem Submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {u : Submonoid (M × N)} :
theorem AddSubmonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {u : AddSubmonoid (M × N)} :
u u u
theorem Submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {u : Submonoid (M × N)} :
theorem AddMonoidHom.mrange.proof_1 {M : Type u_2} {N : Type u_1} {F : Type u_3} [FunLike F M N] (f : F) :
= f '' Set.univ
def AddMonoidHom.mrange {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :

The range of an AddMonoidHom is an AddSubmonoid.

Equations
Instances For
def MonoidHom.mrange {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :

The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].

Equations
Instances For
@[simp]
theorem AddMonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
=
@[simp]
theorem MonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
() =
@[simp]
theorem AddMonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] {f : F} {y : N} :
∃ (x : M), f x = y
@[simp]
theorem MonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] {f : F} {y : N} :
∃ (x : M), f x = y
theorem AddMonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
theorem MonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
theorem AddMonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (g : N →+ P) (f : M →+ N) :
theorem MonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (g : N →* P) (f : M →* N) :
theorem AddMonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] {f : F} :
theorem MonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] {f : F} :
@[simp]
theorem AddMonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) (hf : ) :

The range of a surjective AddMonoid hom is the whole of the codomain.

@[simp]
theorem MonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) (hf : ) :

The range of a surjective monoid hom is the whole of the codomain.

theorem AddMonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) (s : Set N) :
theorem MonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) (s : Set N) :
theorem AddMonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) (s : Set M) :

The image under an AddMonoid hom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set.

theorem MonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) (s : Set M) :

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.

def AddMonoidHom.restrict {M : Type u_1} [] {N : Type u_6} {S : Type u_7} [] [SetLike S M] [] (f : M →+ N) (s : S) :
s →+ N

Restriction of an AddMonoid hom to an AddSubmonoid of the domain.

Equations
Instances For
def MonoidHom.restrict {M : Type u_1} [] {N : Type u_6} {S : Type u_7} [] [SetLike S M] [] (f : M →* N) (s : S) :
s →* N

Restriction of a monoid hom to a submonoid of the domain.

Equations
Instances For
@[simp]
theorem AddMonoidHom.restrict_apply {M : Type u_1} [] {N : Type u_6} {S : Type u_7} [] [SetLike S M] [] (f : M →+ N) (s : S) (x : s) :
() x = f x
@[simp]
theorem MonoidHom.restrict_apply {M : Type u_1} [] {N : Type u_6} {S : Type u_7} [] [SetLike S M] [] (f : M →* N) (s : S) (x : s) :
() x = f x
@[simp]
theorem AddMonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) :
@[simp]
theorem MonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →* N) :
theorem AddMonoidHom.codRestrict.proof_2 {M : Type u_3} {N : Type u_1} [] [] {S : Type u_2} [SetLike S N] [] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) (x : M) (y : M) :
{ toFun := fun (n : M) => { val := f n, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }.toFun x + { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }.toFun y
def AddMonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [] [] {S : Type u_6} [SetLike S N] [] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) :
M →+ s

Restriction of an AddMonoid hom to an AddSubmonoid of the codomain.

Equations
• = { toZeroHom := { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }, map_add' := }
Instances For
theorem AddMonoidHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} [] [] {S : Type u_2} [SetLike S N] [] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) :
(fun (n : M) => { val := f n, property := }) 0 = 0
@[simp]
theorem MonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [] [] {S : Type u_6} [SetLike S N] [] (f : M →* N) (s : S) (h : ∀ (x : M), f x s) (n : M) :
() n = { val := f n, property := }
@[simp]
theorem AddMonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [] [] {S : Type u_6} [SetLike S N] [] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) (n : M) :
() n = { val := f n, property := }
def MonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [] [] {S : Type u_6} [SetLike S N] [] (f : M →* N) (s : S) (h : ∀ (x : M), f x s) :
M →* s

Restriction of a monoid hom to a submonoid of the codomain.

Equations
• = { toOneHom := { toFun := fun (n : M) => { val := f n, property := }, map_one' := }, map_mul' := }
Instances For
def AddMonoidHom.mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →+ N) :
M →+

Restriction of an AddMonoid hom to its range interpreted as a submonoid.

Equations
Instances For
theorem AddMonoidHom.mrangeRestrict.proof_1 {M : Type u_1} [] {N : Type u_2} [] (f : M →+ N) (x : M) :
∃ (y : M), f y = f x
def MonoidHom.mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →* N) :
M →* ()

Restriction of a monoid hom to its range interpreted as a submonoid.

Equations
Instances For
@[simp]
theorem AddMonoidHom.coe_mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →+ N) (x : M) :
() = f x
@[simp]
theorem MonoidHom.coe_mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →* N) (x : M) :
() = f x
abbrev AddMonoidHom.mrangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (motive : Prop) :
∀ (x : ), (∀ (x : M), motive { val := f x, property := })motive x
Equations
• =
Instances For
theorem AddMonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) :
theorem MonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) :
def AddMonoidHom.mker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :

The additive kernel of an AddMonoid hom is the AddSubmonoid of elements such that f x = 0

Equations
Instances For
def MonoidHom.mker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :

The multiplicative kernel of a monoid hom is the submonoid of elements x : G such that f x = 1

Equations
Instances For
theorem AddMonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) {x : M} :
f x = 0
theorem MonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) {x : M} :
f x = 1
theorem AddMonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
= f ⁻¹' {0}
theorem MonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
() = f ⁻¹' {1}
instance AddMonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] [] (f : F) :
DecidablePred fun (x : M) =>
Equations
instance MonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] [] (f : F) :
DecidablePred fun (x : M) =>
Equations
theorem AddMonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (g : N →+ P) (f : M →+ N) :
theorem MonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (g : N →* P) (f : M →* N) :
@[simp]
theorem AddMonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
@[simp]
theorem MonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
@[simp]
theorem AddMonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) :
@[simp]
theorem MonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →* N) :
theorem AddMonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) :
theorem MonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) :
@[simp]
theorem AddMonoidHom.mker_zero {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem MonoidHom.mker_one {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [] [] {M' : Type u_6} {N' : Type u_7} [] [] (f : M →+ N) (g : M' →+ N') (S : ) (S' : ) :
=
theorem MonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [] [] {M' : Type u_6} {N' : Type u_7} [] [] (f : M →* N) (g : M' →* N') (S : ) (S' : ) :
theorem AddMonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [] [] {M' : Type u_6} {N' : Type u_7} [] [] (f : M →+ N) (g : M' →+ N') :
theorem MonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [] [] {M' : Type u_6} {N' : Type u_7} [] [] (f : M →* N) (g : M' →* N') :
@[simp]
theorem AddMonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem MonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddMonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem MonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddMonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem MonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddMonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem MonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoidHom.addSubmonoidComap.proof_3 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) (x : ()) (y : ()) :
{ toFun := fun (x : ()) => { val := f x, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (x : ()) => { val := f x, property := }, map_zero' := }.toFun x + { toFun := fun (x : ()) => { val := f x, property := }, map_zero' := }.toFun y
theorem AddMonoidHom.addSubmonoidComap.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (N' : ) :
(fun (x : ()) => { val := f x, property := }) 0 = 0
def AddMonoidHom.addSubmonoidComap {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) :
() →+ N'

the AddMonoidHom from the preimage of an additive submonoid to itself.

Equations
• = { toZeroHom := { toFun := fun (x : ()) => { val := f x, property := }, map_zero' := }, map_add' := }
Instances For
theorem AddMonoidHom.addSubmonoidComap.proof_1 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) (x : ()) :
x
@[simp]
theorem AddMonoidHom.addSubmonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) (x : ()) :
( x) = f x
@[simp]
theorem MonoidHom.submonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (N' : ) (x : ()) :
(() x) = f x
def MonoidHom.submonoidComap {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (N' : ) :
() →* N'

The MonoidHom from the preimage of a submonoid to itself.

Equations
• = { toOneHom := { toFun := fun (x : ()) => { val := f x, property := }, map_one' := }, map_mul' := }
Instances For
theorem AddMonoidHom.addSubmonoidMap.proof_3 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) (x : M') (y : M') :
{ toFun := fun (x : M') => { val := f x, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }.toFun x + { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }.toFun y
theorem AddMonoidHom.addSubmonoidMap.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (M' : ) :
(fun (x : M') => { val := f x, property := }) 0 = 0
theorem AddMonoidHom.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) (x : M') :
∃ a ∈ M', f a = f x
def AddMonoidHom.addSubmonoidMap {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) :
M' →+ ()

the AddMonoidHom from an additive submonoid to its image. See AddEquiv.AddSubmonoidMap for a variant for AddEquivs.

Equations
• = { toZeroHom := { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }, map_add' := }
Instances For
@[simp]
theorem MonoidHom.submonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (M' : ) (x : M') :
(() x) = f x
@[simp]
theorem AddMonoidHom.addSubmonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) (x : M') :
(() x) = f x
def MonoidHom.submonoidMap {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (M' : ) :
M' →* ()

The MonoidHom from a submonoid to its image. See MulEquiv.SubmonoidMap for a variant for MulEquivs.

Equations
• = { toOneHom := { toFun := fun (x : M') => { val := f x, property := }, map_one' := }, map_mul' := }
Instances For
theorem AddMonoidHom.addSubmonoidMap_surjective {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) :
theorem MonoidHom.submonoidMap_surjective {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (M' : ) :
theorem AddSubmonoid.mrange_inl {M : Type u_1} {N : Type u_2} [] [] :
theorem Submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [] [] :
theorem AddSubmonoid.mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
theorem Submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
theorem AddSubmonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [] [] :
theorem Submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [] [] :
=
theorem AddSubmonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [] [] :
theorem Submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [] [] :
=
@[simp]
theorem AddSubmonoid.mrange_fst {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddSubmonoid.mrange_snd {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [] [] :
theorem AddSubmonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } :
s = t =
theorem Submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } :
= s = t =
theorem AddSubmonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } :