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

source
def add_subgroup.opposite {G : Type u_1} [add_group G] :
add_subgroup G ≃ add_subgroup Gᵃᵒᵖ

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

Equations
source
def subgroup.opposite {G : Type u_1} [group G] :
subgroup G ≃ subgroup Gᵐᵒᵖ

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

Equations
source
def subgroup.opposite_equiv {G : Type u_1} [group G] (H : subgroup G) :
↥H ≃ ↥(⇑subgroup.opposite H)

Bijection between a subgroup H and its opposite.

Equations
source
def add_subgroup.opposite_equiv {G : Type u_1} [add_group G] (H : add_subgroup G) :
↥H ≃ ↥(⇑add_subgroup.opposite H)

Bijection between an additive subgroup H and its opposite.

Equations
source
@[simp]
theorem subgroup.opposite_equiv_symm_apply_coe {G : Type u_1} [group G] (H : subgroup G) (b : {b // (λ (x : Gᵐᵒᵖ), x ∈ ⇑subgroup.opposite H) b}) :
↑(⇑(H.opposite_equiv.symm) b) = mul_opposite.unop ↑b
source
@[simp]
theorem add_subgroup.opposite_equiv_symm_apply_coe {G : Type u_1} [add_group G] (H : add_subgroup G) (b : {b // (λ (x : Gᵃᵒᵖ), x ∈ ⇑add_subgroup.opposite H) b}) :
↑(⇑(H.opposite_equiv.symm) b) = add_opposite.unop ↑b
source
@[simp]
theorem subgroup.opposite_equiv_apply_coe {G : Type u_1} [group G] (H : subgroup G) (a : {a // (λ (x : G), x ∈ H) a}) :
↑(⇑(H.opposite_equiv) a) = mul_opposite.op ↑a
source
@[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}) :
↑(⇑(H.opposite_equiv) a) = add_opposite.op ↑a
source
@[protected, instance]
def add_subgroup.opposite.encodable {G : Type u_1} [add_group G] (H : add_subgroup G) [encodable ↥H] :
encodable ↥(⇑add_subgroup.opposite H)
Equations
source
@[protected, instance]
def subgroup.opposite.encodable {G : Type u_1} [group G] (H : subgroup G) [encodable ↥H] :
encodable ↥(⇑subgroup.opposite H)
Equations
source
@[protected, instance]
def add_subgroup.opposite.countable {G : Type u_1} [add_group G] (H : add_subgroup G) [countable ↥H] :
countable ↥(⇑add_subgroup.opposite H)
source
@[protected, instance]
def subgroup.opposite.countable {G : Type u_1} [group G] (H : subgroup G) [countable ↥H] :
countable ↥(⇑subgroup.opposite H)
source
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)
source
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