Documentation

Mathlib.GroupTheory.Submonoid.MulOpposite

Submonoid of opposite monoids #

For every monoid M, we construct an equivalence between submonoids of M and that of Mᵐᵒᵖ.

theorem AddSubmonoid.op.proof_1 {M : Type u_1} [] (x : ) :
def AddSubmonoid.op {M : Type u_2} [] (x : ) :

Pull an additive submonoid back to an opposite submonoid along AddOpposite.unop

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddSubmonoid.op_coe {M : Type u_2} [] (x : ) :
@[simp]
theorem Submonoid.op_coe {M : Type u_2} [] (x : ) :
() = MulOpposite.unop ⁻¹' x.toSubsemigroup
def Submonoid.op {M : Type u_2} [] (x : ) :

Pull a submonoid back to an opposite submonoid along MulOpposite.unop

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubmonoid.unop.proof_1 {M : Type u_1} [] (x : ) :
∀ {a b : M}, a AddOpposite.op ⁻¹' x.toAddSubsemigroupb AddOpposite.op ⁻¹' x.toAddSubsemigroup{ unop' := b } + { unop' := a } x
theorem AddSubmonoid.unop.proof_2 {M : Type u_1} [] (x : ) :
0 x.carrier
def AddSubmonoid.unop {M : Type u_2} [] (x : ) :

Pull an opposite additive submonoid back to a submonoid along AddOpposite.op

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddSubmonoid.unop_coe {M : Type u_2} [] (x : ) :
@[simp]
theorem Submonoid.unop_coe {M : Type u_2} [] (x : ) :
() = MulOpposite.op ⁻¹' x.toSubsemigroup
def Submonoid.unop {M : Type u_2} [] (x : ) :

Pull an opposite submonoid back to a submonoid along MulOpposite.op

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AddSubmonoid.opEquiv {M : Type u_1} [] :

A additive submonoid H of G determines an additive submonoid H.op of the opposite group Gᵐᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubmonoid.opEquiv.proof_2 {M : Type u_1} [] :
∀ (x : ),
theorem AddSubmonoid.opEquiv.proof_1 {M : Type u_1} [] :
∀ (x : ),
@[simp]
theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_1} [] (x : ) :
@[simp]
theorem AddSubmonoid.opEquiv_apply {M : Type u_1} [] (x : ) :
@[simp]
theorem Submonoid.opEquiv_symm_apply {M : Type u_1} [] (x : ) :
Submonoid.opEquiv.symm x =
@[simp]
theorem Submonoid.opEquiv_apply {M : Type u_1} [] (x : ) :
Submonoid.opEquiv x =
def Submonoid.opEquiv {M : Type u_1} [] :

A submonoid H of G determines a submonoid H.op of the opposite group Gᵐᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [] (H : ) :
∀ (x : M), x H x H
def AddSubmonoid.equivOp {M : Type u_1} [] (H : ) :
H ()

Bijection between an additive submonoid H and its opposite.

Equations
Instances For
@[simp]
theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_1} [] (H : ) (b : { b : Mᵃᵒᵖ // (fun (x : Mᵃᵒᵖ) => ) b }) :
(.symm b) =
@[simp]
theorem Submonoid.equivOp_symm_apply_coe {M : Type u_1} [] (H : ) (b : { b : Mᵐᵒᵖ // (fun (x : Mᵐᵒᵖ) => ) b }) :
(.symm b) =
@[simp]
theorem Submonoid.equivOp_apply_coe {M : Type u_1} [] (H : ) (a : { a : M // (fun (x : M) => x H) a }) :
( a) =
@[simp]
theorem AddSubmonoid.equivOp_apply_coe {M : Type u_1} [] (H : ) (a : { a : M // (fun (x : M) => x H) a }) :
( a) =
def Submonoid.equivOp {M : Type u_1} [] (H : ) :
H ()

Bijection between a submonoid H and its opposite.

Equations
Instances For