def
AddSubgroup.opposite.proof_7
{G : Type u_1}
[inst : AddGroup G]
:
∀ (x : AddSubgroup Gᵃᵒᵖ),
(fun H =>
{
toAddSubmonoid :=
{
toAddSubsemigroup :=
{ carrier := AddOpposite.unop ⁻¹' ↑H,
add_mem' :=
(_ :
∀ {a b : Gᵃᵒᵖ},
a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → b.unop + a.unop ∈ H) },
zero_mem' := (_ : 0 ∈ H) },
neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, x.unop ∈ H → -x.unop ∈ H) })
((fun H =>
{
toAddSubmonoid :=
{
toAddSubsemigroup :=
{ carrier := AddOpposite.op ⁻¹' ↑H,
add_mem' :=
(_ :
∀ {a b : G},
a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop := b } + { unop := a } ∈ H) },
zero_mem' := (_ : 0 ∈ H) },
neg_mem' := (_ : ∀ {x : G}, { unop := x } ∈ H → -{ unop := x } ∈ H) })
x) = x
Equations
- One or more equations did not get rendered due to their size.
An additive subgroup H
of G
determines an additive subgroup H.opposite
of the
opposite additive group Gᵃᵒᵖ
.
Equations
- One or more equations did not get rendered due to their size.
def
AddSubgroup.opposite.proof_6
{G : Type u_1}
[inst : AddGroup G]
:
∀ (x : AddSubgroup G),
(fun H =>
{
toAddSubmonoid :=
{
toAddSubsemigroup :=
{ carrier := AddOpposite.op ⁻¹' ↑H,
add_mem' :=
(_ :
∀ {a b : G},
a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop := b } + { unop := a } ∈ H) },
zero_mem' := (_ : 0 ∈ H) },
neg_mem' := (_ : ∀ {x : G}, { unop := x } ∈ H → -{ unop := x } ∈ H) })
((fun H =>
{
toAddSubmonoid :=
{
toAddSubsemigroup :=
{ carrier := AddOpposite.unop ⁻¹' ↑H,
add_mem' :=
(_ :
∀ {a b : Gᵃᵒᵖ},
a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → b.unop + a.unop ∈ H) },
zero_mem' := (_ : 0 ∈ H) },
neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, x.unop ∈ H → -x.unop ∈ H) })
x) = x
Equations
- One or more equations did not get rendered due to their size.
Bijection between an additive subgroup H
and its opposite.
Equations
- AddSubgroup.oppositeEquiv H = Equiv.subtypeEquiv AddOpposite.opEquiv (_ : ∀ (x : G), x ∈ H ↔ x ∈ H)
@[simp]
theorem
AddSubgroup.oppositeEquiv_apply_coe_unop
{G : Type u_1}
[inst : AddGroup G]
(H : AddSubgroup G)
(a : { a // (fun x => x ∈ H) a })
:
(↑(↑(AddSubgroup.oppositeEquiv H) a)).unop = ↑a
@[simp]
theorem
Subgroup.oppositeEquiv_symm_apply_coe
{G : Type u_1}
[inst : Group G]
(H : Subgroup G)
(b : { b // (fun x => x ∈ ↑Subgroup.opposite H) b })
:
↑(↑(Equiv.symm (Subgroup.oppositeEquiv H)) b) = (↑b).unop
@[simp]
theorem
AddSubgroup.oppositeEquiv_symm_apply_coe
{G : Type u_1}
[inst : AddGroup G]
(H : AddSubgroup G)
(b : { b // (fun x => x ∈ ↑AddSubgroup.opposite H) b })
:
↑(↑(Equiv.symm (AddSubgroup.oppositeEquiv H)) b) = (↑b).unop
@[simp]
theorem
Subgroup.oppositeEquiv_apply_coe_unop
{G : Type u_1}
[inst : Group G]
(H : Subgroup G)
(a : { a // (fun x => x ∈ H) a })
:
(↑(↑(Subgroup.oppositeEquiv H) a)).unop = ↑a
Bijection between a subgroup H
and its opposite.
Equations
- Subgroup.oppositeEquiv H = Equiv.subtypeEquiv MulOpposite.opEquiv (_ : ∀ (x : G), x ∈ H ↔ x ∈ H)
instance
AddSubgroup.instEncodableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite
{G : Type u_1}
[inst : AddGroup G]
(H : AddSubgroup G)
[inst : Encodable { x // x ∈ H }]
:
Equations
- One or more equations did not get rendered due to their size.
def
AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite.proof_1
{G : Type u_1}
[inst : AddGroup G]
(H : AddSubgroup G)
[inst : Countable { x // x ∈ H }]
:
instance
AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite
{G : Type u_1}
[inst : AddGroup G]
(H : AddSubgroup G)
[inst : Countable { x // x ∈ H }]
:
Equations
- One or more equations did not get rendered due to their size.