# 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_apply_coe {M : Type u_1} [] (S : ) :
@[simp]
theorem Submonoid.toAddSubmonoid_symm_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
@[reducible, inline]
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 (Additive M)) :
@[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
@[reducible, inline]
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_3} {N : Type u_1} [] [] {F : Type u_2} [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
• = { 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
• = { 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) :
(Submonoid.comap f S) = 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) :
= Submonoid.comap (g.comp f) S
@[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_2 {M : Type u_1} {N : Type u_2} [] [] {F : Type u_3} [FunLike F M N] [mc : ] (f : F) (S : ) :
aS, f a = 0
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
• = { carrier := f '' S, add_mem' := , zero_mem' := }
Instances For
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
• = { 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 : ) :
(AddSubmonoid.map 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 : ) :
(Submonoid.map 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 xS, 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 xS, 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 : { x : M // 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 : { x : M // 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) :
@[simp]
theorem AddSubmonoid.map_id {M : Type u_1} [] (S : ) :
= S
@[simp]
theorem Submonoid.map_id {M : Type u_1} [] (S : ) :
= 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
• = .toGaloisCoinsertion
Instances For
theorem AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [] [] {F : Type u_3} [FunLike F M N] [mc : ] {f : F} (hf : ) (S : ) (x : M) :
x x S
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
• = .toGaloisCoinsertion
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 : ) :
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
• = .toGaloisInsertion
Instances For
theorem AddSubmonoid.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [] [] {F : Type u_3} [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
• = .toGaloisInsertion
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 { x : M₁ // x S' }

An AddSubmonoid of an AddMonoid inherits a zero.

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

A submonoid of a monoid inherits a 1.

Equations
• = { one := 1, }
@[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 : { x : M₁ // 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 : { x : M₁ // 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 = 0,
theorem OneMemClass.one_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
1 = 1,
instance AddSubmonoidClass.nSMul {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] (S : A) :
SMul { x : M // x S }

An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

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

A submonoid of a monoid inherits a power operator.

Equations
• = { pow := fun (a : { x : M // x S }) (n : ) => a ^ n, }
@[simp]
theorem AddSubmonoidClass.coe_nsmul {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] {S : A} (x : { x : M // 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 : { x : M // 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 x, hx = n x,
@[simp]
theorem SubmonoidClass.mk_pow {M : Type u_6} [] {A : Type u_5} [SetLike A M] [] {S : A} (x : M) (hx : x S) (n : ) :
x, hx ^ n = x ^ n,
@[instance 75]
instance AddSubmonoidClass.toAddZeroClass {M : Type u_5} [] {A : Type u_6} [SetLike A M] [] (S : A) :
AddZeroClass { x : M // x S }

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

Equations
theorem AddSubmonoidClass.toAddZeroClass.proof_2 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
0 = 0
theorem AddSubmonoidClass.toAddZeroClass.proof_3 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x x_1 : { x : M // x S }), (x + x_1) = (x + x_1)
theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
Function.Injective fun (a : { x : M // x S }) => a
@[instance 75]
instance SubmonoidClass.toMulOneClass {M : Type u_5} [] {A : Type u_6} [SetLike A M] [] (S : A) :
MulOneClass { x : M // x S }

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

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

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

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

A submonoid of a monoid inherits a monoid structure.

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

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

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

A submonoid of a CommMonoid is a CommMonoid.

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

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

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

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

Equations
• = { 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
Add { x : M // x S }

An AddSubmonoid of an AddMonoid inherits an addition.

Equations
• S.add = { add := fun (a b : { x : M // x S }) => a + b, }
theorem AddSubmonoid.add.proof_1 {M : Type u_1} [] (S : ) (a : { x : M // x S }) (b : { x : M // x S }) :
a + b S
instance Submonoid.mul {M : Type u_1} [] (S : ) :
Mul { x : M // x S }

A submonoid of a monoid inherits a multiplication.

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

An AddSubmonoid of an AddMonoid inherits a zero.

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

A submonoid of a monoid inherits a 1.

Equations
• S.one = { one := 1, }
@[simp]
theorem AddSubmonoid.coe_add {M : Type u_1} [] (S : ) (x : { x : M // x S }) (y : { x : M // x S }) :
(x + y) = x + y
@[simp]
theorem Submonoid.coe_mul {M : Type u_1} [] (S : ) (x : { x : M // x S }) (y : { x : M // x 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} :
a, ha = 0 a = 0
@[simp]
theorem Submonoid.mk_eq_one {M : Type u_1} [] (S : ) {a : M} {ha : a S} :
a, 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) :
x, hx + y, hy = x + y,
@[simp]
theorem Submonoid.mk_mul_mk {M : Type u_1} [] (S : ) (x : M) (y : M) (hx : x S) (hy : y S) :
x, hx * y, hy = x * y,
theorem AddSubmonoid.add_def {M : Type u_1} [] (S : ) (x : { x : M // x S }) (y : { x : M // x S }) :
x + y = x + y,
theorem Submonoid.mul_def {M : Type u_1} [] (S : ) (x : { x : M // x S }) (y : { x : M // x S }) :
x * y = x * y,
theorem AddSubmonoid.zero_def {M : Type u_1} [] (S : ) :
0 = 0,
theorem Submonoid.one_def {M : Type u_1} [] (S : ) :
1 = 1,
Function.Injective fun (a : { x : M // x S }) => a
∀ (x x_1 : { x : M // x S }), (x + x_1) = (x + x_1)
AddZeroClass { x : M // x S }

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

Equations
0 = 0
instance Submonoid.toMulOneClass {M : Type u_5} [] (S : ) :
MulOneClass { x : M // x 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
Function.Injective fun (a : { x : M // x S }) => a
0 = 0
∀ (x x_1 : { x : M // x S }), (x + x_1) = (x + x_1)
AddMonoid { x : M // x S }

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations
∀ (x : { x : M // x S }) (x_1 : ), (x_1 x) = (x_1 x)
instance Submonoid.toMonoid {M : Type u_5} [] (S : ) :
Monoid { x : M // x S }

A submonoid of a monoid inherits a monoid structure.

Equations
0 = 0
Function.Injective fun (a : { x : M // x S }) => a
AddCommMonoid { x : M // x S }

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations
∀ (x : { x : M // x S }) (x_1 : ), (x_1 x) = (x_1 x)
∀ (x x_1 : { x : M // x S }), (x + x_1) = (x + x_1)
instance Submonoid.toCommMonoid {M : Type u_5} [] (S : ) :
CommMonoid { x : M // x S }

A submonoid of a CommMonoid is a CommMonoid.

Equations
theorem AddSubmonoid.subtype.proof_1 {M : Type u_1} [] (S : ) :
0 = 0
def AddSubmonoid.subtype {M : Type u_1} [] (S : ) :
{ x : M // x S } →+ M

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

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

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

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

Equations
• AddSubmonoid.topEquiv = { toFun := fun (x : { x : M // x }) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_add' := }
Instances For
theorem AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [] (x : { x : M // x }) :
x, = x
theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [] :
∀ (x : M), (fun (x : { x : M // x }) => x) ((fun (x : M) => x, ) x) = (fun (x : { x : M // x }) => x) ((fun (x : M) => x, ) x)
theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [] :
∀ (x x_1 : { x : M // x }), { toFun := fun (x : { x : M // x }) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : { x : M // x }) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := }.toFun (x + x_1)
@[simp]
theorem AddSubmonoid.topEquiv_apply {M : Type u_1} [] (x : { x : M // x }) :
@[simp]
theorem AddSubmonoid.topEquiv_symm_apply_coe {M : Type u_1} [] (x : M) :
@[simp]
theorem Submonoid.topEquiv_apply {M : Type u_1} [] (x : { x : M // x }) :
Submonoid.topEquiv x = x
@[simp]
theorem Submonoid.topEquiv_symm_apply_coe {M : Type u_1} [] (x : M) :
(Submonoid.topEquiv.symm x) = x
def Submonoid.topEquiv {M : Type u_1} [] :
{ x : M // x } ≃* M

The top submonoid is isomorphic to the monoid.

Equations
• Submonoid.topEquiv = { toFun := fun (x : { x : M // x }) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_mul' := }
Instances For
@[simp]
@[simp]
theorem Submonoid.topEquiv_toMonoidHom {M : Type u_1} [] :
Submonoid.topEquiv = .subtype
noncomputable def AddSubmonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) (hf : ) :
{ x : M // x S } ≃+ { x : N // x }

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
• S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := }
Instances For
theorem AddSubmonoid.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) (hf : ) :
∀ (x x_1 : { x : M // x 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 Submonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →* N) (hf : ) :
{ x : M // x S } ≃* { x : N // x }

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

Equations
• S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := }
Instances For
@[simp]
theorem AddSubmonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →+ N) (hf : ) (x : { x : M // x S }) :
((S.equivMapOfInjective f hf) x) = f x
@[simp]
theorem Submonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [] [] (S : ) (f : M →* N) (hf : ) (x : { x : M // x S }) :
((S.equivMapOfInjective f hf) 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
• s.prod t = { 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
• s.prod t = { carrier := s ×ˢ t, mul_mem' := , one_mem' := }
Instances For
theorem AddSubmonoid.coe_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
(s.prod t) = s ×ˢ t
theorem Submonoid.coe_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
(s.prod t) = s ×ˢ t
theorem AddSubmonoid.mem_prod {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {p : M × N} :
p s.prod t p.1 s p.2 t
theorem Submonoid.mem_prod {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {p : M × N} :
p s.prod t 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₂) :
s₁.prod t₁ s₂.prod t₂
theorem Submonoid.prod_mono {M : Type u_1} {N : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem AddSubmonoid.prod_top {M : Type u_1} {N : Type u_2} [] [] (s : ) :
s.prod =
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 : ) :
.prod 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} [] [] :
.prod =
@[simp]
theorem Submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [] [] :
.prod =
theorem AddSubmonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [] [] :
.prod =
theorem Submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [] [] :
.prod =
def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
{ x : M × N // x s.prod t } ≃+ { x : M // x s } × { x : N // x t }

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

Equations
Instances For
theorem AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
∀ (x x_1 : { x : M × N // x s.prod t }), (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 : ) :
{ x : M × N // x s.prod t } ≃* { x : M // x s } × { x : N // x t }

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

Equations
Instances For
theorem AddSubmonoid.map_inl {M : Type u_1} {N : Type u_2} [] [] (s : ) :
= s.prod
theorem Submonoid.map_inl {M : Type u_1} {N : Type u_2} [] [] (s : ) :
theorem AddSubmonoid.map_inr {M : Type u_1} {N : Type u_2} [] [] (s : ) :
= .prod s
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 : ) :
s.prod .prod t = s.prod t
@[simp]
theorem Submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [] [] (s : ) (t : ) :
s.prod .prod t = s.prod t
theorem AddSubmonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [] [] {f : M ≃+ N} {K : } {x : N} :
theorem Submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [] [] {f : M ≃* N} {K : } {x : N} :
x Submonoid.map f.toMonoidHom K f.symm 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 : ) :
Submonoid.map f.toMonoidHom K = Submonoid.comap f.symm.toMonoidHom 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 : ) :
= Submonoid.map f.symm 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.prod t 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)} :
s.prod t u u u
theorem Submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } {u : Submonoid (M × N)} :
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
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 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) :
@[simp]
theorem AddMonoidHom.mrange_id {M : Type u_1} [] :
@[simp]
theorem MonoidHom.mrange_id {M : Type u_1} [] :
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) :
= MonoidHom.mrange (g.comp f)
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.

@[simp]
theorem AddMonoidHom.mclosure_range {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
@[simp]
theorem MonoidHom.mclosure_range {M : Type u_1} {N : Type u_2} [] [] {F : Type u_5} [FunLike F M N] [mc : ] (f : F) :
def AddMonoidHom.restrict {M : Type u_1} [] {N : Type u_6} {S : Type u_7} [] [SetLike S M] [] (f : M →+ N) (s : S) :
{ x : M // x s } →+ N

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

Equations
• f.restrict s = f.comp
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) :
{ x : M // x s } →* N

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

Equations
• f.restrict s = f.comp
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 : { x : M // x s }) :
(f.restrict 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 : { x : M // x s }) :
(f.restrict 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) :
MonoidHom.mrange (f.restrict S) =
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) => f n, , map_zero' := }.toFun (x + y) = { toFun := fun (n : M) => f n, , map_zero' := }.toFun x + { toFun := fun (n : M) => f n, , map_zero' := }.toFun y
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) => f n, ) 0 = 0
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 →+ { x : N // x s }

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

Equations
• f.codRestrict s h = { toFun := fun (n : M) => f n, , map_zero' := , map_add' := }
Instances For
@[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) :
(f.codRestrict s h) n = f n,
@[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) :
(f.codRestrict s h) n = f n,
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 →* { x : N // x s }

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

Equations
• f.codRestrict s h = { toFun := fun (n : M) => f n, , map_one' := , map_mul' := }
Instances For
@[simp]
theorem AddMonoidHom.injective_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) :
Function.Injective (f.codRestrict s h)
@[simp]
theorem MonoidHom.injective_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) :
Function.Injective (f.codRestrict s h)
def AddMonoidHom.mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →+ N) :
M →+ { x : N // }

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

Equations
• f.mrangeRestrict = f.codRestrict
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 →* { x : N // }

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

Equations
• f.mrangeRestrict = f.codRestrict
Instances For
@[simp]
theorem AddMonoidHom.coe_mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →+ N) (x : M) :
(f.mrangeRestrict x) = f x
@[simp]
theorem MonoidHom.coe_mrangeRestrict {M : Type u_1} [] {N : Type u_6} [] (f : M →* N) (x : M) :
(f.mrangeRestrict x) = f x
theorem AddMonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) :
Function.Surjective f.mrangeRestrict
theorem MonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) :
Function.Surjective f.mrangeRestrict
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) :
= MonoidHom.mker (g.comp f)
@[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) :
MonoidHom.mker (f.restrict S) = Submonoid.comap S.subtype
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) :
MonoidHom.mker f.mrangeRestrict =
@[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' : ) :
Submonoid.comap (f.prodMap g) (S.prod S') = (Submonoid.comap f S).prod (Submonoid.comap g 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') :
MonoidHom.mker (f.prodMap g) = .prod
@[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} [] [] :
= .prod
@[simp]
theorem MonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [] [] :
= .prod
@[simp]
theorem AddMonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [] [] :
= .prod
@[simp]
theorem MonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [] [] :
= .prod
theorem AddMonoidHom.addSubmonoidComap.proof_1 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) (x : { x : M // x }) :
x
theorem AddMonoidHom.addSubmonoidComap.proof_3 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) (x : { x : M // x }) (y : { x : M // x }) :
{ toFun := fun (x : { x : M // x }) => f x, , map_zero' := }.toFun (x + y) = { toFun := fun (x : { x : M // x }) => f x, , map_zero' := }.toFun x + { toFun := fun (x : { x : M // x }) => f x, , map_zero' := }.toFun y
theorem AddMonoidHom.addSubmonoidComap.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (N' : ) :
(fun (x : { x : M // x }) => f x, ) 0 = 0
def AddMonoidHom.addSubmonoidComap {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (N' : ) :
{ x : M // x } →+ { x : N // x N' }

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

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

The MonoidHom from the preimage of a submonoid to itself.

Equations
• f.submonoidComap N' = { toFun := fun (x : { x : M // x }) => f x, , map_one' := , map_mul' := }
Instances For
theorem AddMonoidHom.addSubmonoidMap.proof_3 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) (x : { x : M // x M' }) (y : { x : M // x M' }) :
{ toFun := fun (x : { x : M // x M' }) => f x, , map_zero' := }.toFun (x + y) = { toFun := fun (x : { x : M // x M' }) => f x, , map_zero' := }.toFun x + { toFun := fun (x : { x : M // x M' }) => f x, , map_zero' := }.toFun y
def AddMonoidHom.addSubmonoidMap {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) :
{ x : M // x M' } →+ { x : N // x }

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

Equations
• f.addSubmonoidMap M' = { toFun := fun (x : { x : M // x M' }) => f x, , map_zero' := , map_add' := }
Instances For
theorem AddMonoidHom.addSubmonoidMap.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (M' : ) :
(fun (x : { x : M // x M' }) => f x, ) 0 = 0
theorem AddMonoidHom.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) (x : { x : M // x M' }) :
aM', f a = f x
@[simp]
theorem AddMonoidHom.addSubmonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (M' : ) (x : { x : M // x M' }) :
((f.addSubmonoidMap M') x) = f x
@[simp]
theorem MonoidHom.submonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (M' : ) (x : { x : M // x M' }) :
((f.submonoidMap M') x) = f x
def MonoidHom.submonoidMap {M : Type u_1} {N : Type u_2} [] [] (f : M →* N) (M' : ) :
{ x : M // x M' } →* { x : N // x }

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

Equations
• f.submonoidMap M' = { toFun := fun (x : { x : M // x M' }) => f x, , 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' : ) :
Function.Surjective (f.submonoidMap M')
theorem AddSubmonoid.mrange_inl {M : Type u_1} {N : Type u_2} [] [] :
= .prod
theorem Submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [] [] :
= .prod
theorem AddSubmonoid.mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
= .prod
theorem Submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
= .prod
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.prod t = s = t =
theorem Submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [] [] {s : } {t : } :
s.prod t = s = t =