# Documentation

Mathlib.GroupTheory.Subgroup.MulOpposite

# Mul-opposite subgroups #

## Tags #

subgroup, subgroups

theorem AddSubgroup.opposite.proof_2 {G : Type u_1} [] (H : ) :
∀ {x : Gᵃᵒᵖ},
theorem AddSubgroup.opposite.proof_5 {G : Type u_1} [] (H : ) :
∀ {x : G},
theorem AddSubgroup.opposite.proof_1 {G : Type u_1} [] (H : ) :
∀ {a b : Gᵃᵒᵖ}, a AddOpposite.unop ⁻¹' Hb AddOpposite.unop ⁻¹' H
theorem AddSubgroup.opposite.proof_4 {G : Type u_1} [] (H : ) :
0 H
def AddSubgroup.opposite {G : Type u_1} [] :

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} [] :
theorem AddSubgroup.opposite.proof_7 {G : Type u_1} [] :
theorem AddSubgroup.opposite.proof_3 {G : Type u_1} [] (H : ) :
∀ {a b : G}, a AddOpposite.op ⁻¹' Hb AddOpposite.op ⁻¹' H{ unop' := b } + { unop' := a } H
def Subgroup.opposite {G : Type u_1} [] :

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

Instances For
theorem AddSubgroup.oppositeEquiv.proof_1 {G : Type u_1} [] (H : ) :
∀ (x : G), x H x H
def AddSubgroup.oppositeEquiv {G : Type u_1} [] (H : ) :
{ x // x H } { x // x AddSubgroup.opposite H }

Bijection between an additive subgroup H and its opposite.

Instances For
@[simp]
theorem Subgroup.oppositeEquiv_symm_apply_coe {G : Type u_1} [] (H : ) (b : { b // (fun x => x Subgroup.opposite H) b }) :
↑(().symm b) =
@[simp]
theorem AddSubgroup.oppositeEquiv_symm_apply_coe {G : Type u_1} [] (H : ) (b : { b // (fun x => x AddSubgroup.opposite H) b }) :
↑(().symm b) =
@[simp]
theorem AddSubgroup.oppositeEquiv_apply_coe {G : Type u_1} [] (H : ) (a : { a // (fun x => x H) a }) :
↑() =
@[simp]
theorem Subgroup.oppositeEquiv_apply_coe {G : Type u_1} [] (H : ) (a : { a // (fun x => x H) a }) :
↑(↑() a) =
def Subgroup.oppositeEquiv {G : Type u_1} [] (H : ) :
{ x // x H } { x // x Subgroup.opposite H }

Bijection between a subgroup H and its opposite.

Instances For
theorem AddSubgroup.vadd_opposite_add {G : Type u_1} [] {H : } (x : G) (g : G) (h : { x // x AddSubgroup.opposite H }) :
h +ᵥ (g + x) = g + (h +ᵥ x)
theorem Subgroup.smul_opposite_mul {G : Type u_1} [] {H : } (x : G) (g : G) (h : { x // x Subgroup.opposite H }) :
h (g * x) = g * h x