mathlib3 documentation

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

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

Equations

Bijection between a subgroup H and its opposite.

Equations

Bijection between an additive subgroup H and its opposite.

Equations
@[simp]
@[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]
theorem add_subgroup.vadd_opposite_add {G : Type u_1} [add_group G] {H : add_subgroup G} (x g : G) (h : (add_subgroup.opposite H)) :
h +ᵥ (g + x) = g + (h +ᵥ x)
theorem subgroup.smul_opposite_mul {G : Type u_1} [group G] {H : subgroup G} (x g : G) (h : (subgroup.opposite H)) :
h (g * x) = g * h x