Theorems · Definition · group theory

Subgroup.unop

{G : Type u_2} → [inst : Group G] → Subgroup Gᵐᵒᵖ → Subgroup G

Pull an opposite subgroup back to a subgroup along MulOpposite.op

Defined in: Mathlib.Algebra.Group.Subgroup.MulOpposite
Cited by: 30 results in Mathlib
Foundations: Depth 27 from the axioms · uses propext, Quot.sound
Assumes: Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

SetLike.coeproof · cited by 8,199
Groupstatement and proof · cited by 6,238
Set.preimageproof · cited by 4,946
Subgroupstatement and proof · cited by 3,593
MulOppositestatement and proof · cited by 1,135
MulOpposite.opproof · cited by 520

Cited by31

Results whose statement or proof uses this declaration.

Subgroup.opEquivproof · cited by 18
Subgroup.op_unopstatement · cited by 3
Subgroup.unop_injectivestatement · cited by 2
Subgroup.normal_unopstatement · cited by 2
Subgroup.unop_topstatement · cited by 1
Subgroup.op_sInfstatement · cited by 1
Subgroup.coe_unopstatement and proof · cited by 1
Subgroup.unop_botstatement · cited by 1
Subgroup.unop_eq_botstatement · cited by 0
Subgroup.unop_eq_topstatement · cited by 0
Subgroup.unop_iInfstatement · cited by 0
Subgroup.unop_iSupstatement · cited by 0