Submonoid of opposite monoids #
For every monoid M
, we construct an equivalence between submonoids of M
and that of Mᵐᵒᵖ
.
Pull an additive submonoid back to an opposite submonoid along
AddOpposite.unop
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Lattice results #
theorem
AddSubmonoid.op_le_iff
{M : Type u_2}
[AddZeroClass M]
{S₁ : AddSubmonoid M}
{S₂ : AddSubmonoid Mᵃᵒᵖ}
:
theorem
AddSubmonoid.le_op_iff
{M : Type u_2}
[AddZeroClass M]
{S₁ : AddSubmonoid Mᵃᵒᵖ}
{S₂ : AddSubmonoid M}
:
@[simp]
@[simp]
@[simp]
A additive submonoid H
of G
determines an additive submonoid
H.op
of the opposite group Gᵐᵒᵖ
.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
AddSubmonoid.op_iSup
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid M)
:
theorem
AddSubmonoid.unop_iSup
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid Mᵃᵒᵖ)
:
theorem
AddSubmonoid.op_iInf
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid M)
:
theorem
AddSubmonoid.unop_iInf
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid Mᵃᵒᵖ)
:
Bijection between a submonoid H
and its opposite.
Equations
Instances For
Bijection between an additive submonoid H
and its opposite.
Equations
Instances For
@[simp]
@[simp]
theorem
AddSubmonoid.equivOp_apply_coe
{M : Type u_2}
[AddZeroClass M]
(H : AddSubmonoid M)
(a : ↥H)
:
@[simp]
theorem
Submonoid.equivOp_symm_apply_coe
{M : Type u_2}
[MulOneClass M]
(H : Submonoid M)
(b : ↥H.op)
:
@[simp]
theorem
AddSubmonoid.equivOp_symm_apply_coe
{M : Type u_2}
[AddZeroClass M]
(H : AddSubmonoid M)
(b : ↥H.op)
: