theorem
AddSubgroup.opposite.proof_2
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
:
∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x ∈ H → -AddOpposite.unop x ∈ H
theorem
AddSubgroup.opposite.proof_5
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup Gᵃᵒᵖ)
:
∀ {x : G}, AddOpposite.op x ∈ H → -AddOpposite.op x ∈ H
theorem
AddSubgroup.opposite.proof_1
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
:
∀ {a b : Gᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → AddOpposite.unop b + AddOpposite.unop a ∈ H
An additive subgroup H
of G
determines an additive subgroup H.opposite
of the
opposite additive group Gᵃᵒᵖ
.
Instances For
theorem
AddSubgroup.opposite.proof_6
{G : Type u_1}
[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}, AddOpposite.op x ∈ H → -AddOpposite.op x ∈ H) })
((fun H =>
{
toAddSubmonoid :=
{
toAddSubsemigroup :=
{ carrier := AddOpposite.unop ⁻¹' ↑H,
add_mem' :=
(_ :
∀ {a b : Gᵃᵒᵖ},
a ∈ AddOpposite.unop ⁻¹' ↑H →
b ∈ AddOpposite.unop ⁻¹' ↑H → AddOpposite.unop b + AddOpposite.unop a ∈ H) },
zero_mem' := (_ : 0 ∈ H) },
neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x ∈ H → -AddOpposite.unop x ∈ H) })
x) = x
theorem
AddSubgroup.opposite.proof_7
{G : Type u_1}
[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 → AddOpposite.unop b + AddOpposite.unop a ∈ H) },
zero_mem' := (_ : 0 ∈ H) },
neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x ∈ H → -AddOpposite.unop x ∈ 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}, AddOpposite.op x ∈ H → -AddOpposite.op x ∈ H) })
x) = x
Bijection between an additive subgroup H
and its opposite.
Instances For
@[simp]
theorem
Subgroup.oppositeEquiv_symm_apply_coe
{G : Type u_1}
[Group G]
(H : Subgroup G)
(b : { b // (fun x => x ∈ ↑Subgroup.opposite H) b })
:
↑(↑(Subgroup.oppositeEquiv H).symm b) = MulOpposite.unop ↑b
@[simp]
theorem
AddSubgroup.oppositeEquiv_symm_apply_coe
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(b : { b // (fun x => x ∈ ↑AddSubgroup.opposite H) b })
:
↑(↑(AddSubgroup.oppositeEquiv H).symm b) = AddOpposite.unop ↑b
@[simp]
theorem
AddSubgroup.oppositeEquiv_apply_coe
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(a : { a // (fun x => x ∈ H) a })
:
↑(↑(AddSubgroup.oppositeEquiv H) a) = AddOpposite.op ↑a
@[simp]
theorem
Subgroup.oppositeEquiv_apply_coe
{G : Type u_1}
[Group G]
(H : Subgroup G)
(a : { a // (fun x => x ∈ H) a })
:
↑(↑(Subgroup.oppositeEquiv H) a) = MulOpposite.op ↑a
instance
AddSubgroup.instEncodableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Encodable { x // x ∈ H }]
:
instance
AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Countable { x // x ∈ H }]
:
theorem
AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite.proof_1
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Countable { x // x ∈ H }]
: