# mathlib3documentation

group_theory.subgroup.mul_opposite

# Mul-opposite subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Tags #

subgroup, subgroups

An additive subgroup H of G determines an additive subgroup H.opposite of the opposite additive group Gᵃᵒᵖ.

Equations
def subgroup.opposite {G : Type u_1} [group G] :

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

Equations
def subgroup.opposite_equiv {G : Type u_1} [group G] (H : subgroup G) :

Bijection between a subgroup H and its opposite.

Equations

Bijection between an additive subgroup H and its opposite.

Equations
@[simp]
theorem subgroup.opposite_equiv_symm_apply_coe {G : Type u_1} [group G] (H : subgroup G) (b : {b // (λ (x : Gᵐᵒᵖ), b}) :
@[simp]
theorem add_subgroup.opposite_equiv_symm_apply_coe {G : Type u_1} [add_group G] (H : add_subgroup G) (b : {b // (λ (x : Gᵃᵒᵖ), b}) :
@[simp]
theorem subgroup.opposite_equiv_apply_coe {G : Type u_1} [group G] (H : subgroup G) (a : {a // (λ (x : G), x H) a}) :
@[simp]
theorem add_subgroup.opposite_equiv_apply_coe {G : Type u_1} [add_group G] (H : add_subgroup G) (a : {a // (λ (x : G), x H) a}) :
@[protected, instance]
Equations
@[protected, instance]
def subgroup.opposite.encodable {G : Type u_1} [group G] (H : subgroup G) [encodable H] :
Equations
@[protected, instance]
@[protected, instance]
def subgroup.opposite.countable {G : Type u_1} [group G] (H : subgroup G) [countable H] :