Mathlib Map

Theorems · Definition · group theory

SemidirectProduct.right

{N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N ⋊[φ] G → G

The element of G

Defined in
Mathlib.GroupTheory.SemidirectProduct
Cited by
35 results in Mathlib
Foundations
Depth 24 from the axioms · uses Quot.sound
Assumes
GroupGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SemidirectProduct.rightHom · cited by 9SemidirectProduct.rightHomSemidirectProduct.map · cited by 8SemidirectProduct.mapSemidirectProduct.ext · cited by 7SemidirectProduct.extSemidirectProduct.lift · cited by 7SemidirectProduct.liftSemidirectProduct.congr · cited by 4SemidirectProduct.congrSemidirectProduct.equivProd · cited by 4SemidirectProduct.equivPr…CategoryTheory.ActionCategory.uncurry · cited by 2ActionCategory.uncurrySemidirectProduct.inl_aut · cited by 1SemidirectProduct.inl_autSemidirectProduct.inl_left_mul_inr_right · cited by 1SemidirectProduct.inl_lef…SemidirectProduct.inr_injective · cited by 1SemidirectProduct.inr_inj…SemidirectProduct.lift_unique · cited by 1SemidirectProduct.lift_un…SemidirectProduct.map_inl · cited by 1SemidirectProduct.map_inlSemidirectProduct.range_inl_eq_ker_rightHom · cited by 1SemidirectProduct.range_i…SemidirectProduct.rightHom_eq_right · cited by 1SemidirectProduct.rightHo…SemidirectProduct.right_inr · cited by 1SemidirectProduct.right_i…Group · cited by 6238GroupMonoidHom · cited by 3629MonoidHomMulAut · cited by 158MulAutSemidirectProduct · cited by 69SemidirectProductSemidirectProduct.rightCITED BYCITES

Cites4

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

Cited by41

Results whose statement or proof uses this declaration.