SemidirectProduct

📁 Source: Mathlib/GroupTheory/SemidirectProduct.lean

Statistics

Metric	Count
Definitions SemidirectProduct, congr', equivProd, inl, inr, instGroup, instInhabited, instInv, instMul, instOne, left, map, monoidHomSubgroup, mulEquivProd, mulEquivSubgroup, right, rightHom, instDecidableEqSemidirectProduct, decEq, «term_⋊[_]_»	20
Theorems card, congr'_apply_left, congr'_apply_right, congr'_symm_apply_left, congr'_symm_apply_right, congr_apply_left, congr_apply_right, congr_symm_apply_left, congr_symm_apply_right, equivProd_apply, equivProd_symm_apply_left, equivProd_symm_apply_right, ext, ext_iff, hom_ext, inl_aut, inl_aut_inv, inl_inj, inl_injective, inl_left_mul_inr_right, inr_inj, inr_injective, inv_left, inv_right, left_inl, left_inr, lift_comp_inl, lift_comp_inr, lift_inl, lift_inr, lift_unique, map_comp_inl, map_comp_inr, map_inl, map_inr, map_left, map_right, mk_eq_inl_mul_inr, monoidHomSubgroup_apply, mulEquivProd_apply, mulEquivProd_symm_apply_left, mulEquivProd_symm_apply_right, mulEquivSubgroup_apply, mulEquivSubgroup_symm_apply, mul_def, mul_left, mul_right, one_left, one_right, range_inl_eq_ker_rightHom, rightHom_comp_inl, rightHom_comp_inr, rightHom_comp_map, rightHom_eq_right, rightHom_inl, rightHom_inr, rightHom_surjective, right_inl, right_inr	59
Total	79

SemidirectProduct

Definitions

Name	Category	Theorems
congr' 📖	CompOp	4 math math: congr'_apply_right, congr'_apply_left, congr'_symm_apply_right, congr'_symm_apply_left
equivProd 📖	CompOp	3 math math: equivProd_apply, equivProd_symm_apply_left, equivProd_symm_apply_right
inl 📖	CompOp	17 math math: rightHom_inl, inl_aut, inl_left_mul_inr_right, map_comp_inl, left_inl, inl_aut_inv, lift_inl, lift_comp_inl, map_inl, rightHom_comp_inl, inl_inj, toGroupExtension_inl, lift_unique, range_inl_eq_ker_rightHom, right_inl, mk_eq_inl_mul_inr, inl_injective
inr 📖	CompOp	15 math math: inl_aut, inr_injective, inr_inj, inl_left_mul_inr_right, lift_inr, rightHom_comp_inr, inl_aut_inv, right_inr, rightHom_inr, map_inr, lift_comp_inr, lift_unique, map_comp_inr, mk_eq_inl_mul_inr, left_inr
instGroup 📖	CompOp	38 math math: rightHom_inl, inl_aut, inr_injective, inr_inj, inl_left_mul_inr_right, lift_inr, map_comp_inl, rightHom_comp_inr, rightHom_surjective, left_inl, inl_aut_inv, right_inr, lift_inl, CategoryTheory.ActionCategory.curry_apply_left, lift_comp_inl, rightHom_eq_right, map_left, rightHom_inr, map_inl, map_inr, rightHom_comp_inl, lift_comp_inr, inl_inj, map_right, toGroupExtension_inl, mulEquivSubgroup_symm_apply, lift_unique, CategoryTheory.ActionCategory.curry_apply_right, map_comp_inr, range_inl_eq_ker_rightHom, right_inl, toGroupExtension_rightHom, mk_eq_inl_mul_inr, right_splitting, left_inr, inl_injective, rightHom_comp_map, monoidHomSubgroup_apply
instInhabited 📖	CompOp	—
instInv 📖	CompOp	2 math math: inv_left, inv_right
instMul 📖	CompOp	20 math math: congr_symm_apply_left, inl_aut, inl_left_mul_inr_right, congr'_apply_right, congr'_apply_left, congr'_symm_apply_right, mul_def, inl_aut_inv, mulEquivProd_symm_apply_left, congr_symm_apply_right, congr'_symm_apply_left, congr_apply_left, congr_apply_right, mulEquivSubgroup_apply, mul_right, mulEquivProd_apply, mulEquivSubgroup_symm_apply, mulEquivProd_symm_apply_right, mul_left, mk_eq_inl_mul_inr
instOne 📖	CompOp	2 math math: one_left, one_right
left 📖	CompOp	21 math math: congr_symm_apply_left, one_left, inl_left_mul_inr_right, CategoryTheory.ActionCategory.uncurry_map, congr'_apply_left, mul_def, left_inl, mulEquivProd_symm_apply_left, CategoryTheory.ActionCategory.curry_apply_left, equivProd_apply, map_left, congr'_symm_apply_left, congr_apply_left, inv_left, mulEquivSubgroup_apply, mulEquivProd_apply, mul_left, left_inr, equivProd_symm_apply_left, monoidHomSubgroup_apply, ext_iff
map 📖	CompOp	7 math math: map_comp_inl, map_left, map_inl, map_inr, map_right, map_comp_inr, rightHom_comp_map
monoidHomSubgroup 📖	CompOp	2 math math: mulEquivSubgroup_symm_apply, monoidHomSubgroup_apply
mulEquivProd 📖	CompOp	3 math math: mulEquivProd_symm_apply_left, mulEquivProd_apply, mulEquivProd_symm_apply_right
mulEquivSubgroup 📖	CompOp	2 math math: mulEquivSubgroup_apply, mulEquivSubgroup_symm_apply
right 📖	CompOp	24 math math: inl_left_mul_inr_right, congr'_apply_right, congr'_symm_apply_right, mul_def, one_right, right_inr, equivProd_apply, rightHom_eq_right, congr_symm_apply_right, congr_apply_right, map_right, inv_left, mulEquivSubgroup_apply, mul_right, inv_right, mulEquivProd_apply, mulEquivProd_symm_apply_right, CategoryTheory.ActionCategory.curry_apply_right, right_inl, mul_left, right_splitting, monoidHomSubgroup_apply, equivProd_symm_apply_right, ext_iff
rightHom 📖	CompOp	9 math math: rightHom_inl, rightHom_comp_inr, rightHom_surjective, rightHom_eq_right, rightHom_inr, rightHom_comp_inl, range_inl_eq_ker_rightHom, toGroupExtension_rightHom, rightHom_comp_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Nat.card SemidirectProduct	—	Nat.card_congr Nat.card_prod
congr'_apply_left 📖	mathematical	—	left MonoidHom.comp MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup MonoidHomClass.toMonoidHom MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MulAut.congr MulEquiv.symm DFunLike.coe SemidirectProduct MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass instMul congr'	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
congr'_apply_right 📖	mathematical	—	right MonoidHom.comp MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup MonoidHomClass.toMonoidHom MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MulAut.congr MulEquiv.symm DFunLike.coe SemidirectProduct MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass instMul congr'	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
congr'_symm_apply_left 📖	mathematical	—	left DFunLike.coe MulEquiv SemidirectProduct MonoidHom.comp MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup MonoidHomClass.toMonoidHom EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulAut.congr MulEquiv.symm instMul congr'	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
congr'_symm_apply_right 📖	mathematical	—	right DFunLike.coe MulEquiv SemidirectProduct MonoidHom.comp MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup MonoidHomClass.toMonoidHom EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulAut.congr MulEquiv.symm instMul congr'	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
congr_apply_left 📖	mathematical	MulEquiv.trans MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike	left SemidirectProduct instMul congr	—	—
congr_apply_right 📖	mathematical	MulEquiv.trans MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike	right SemidirectProduct instMul congr	—	—
congr_symm_apply_left 📖	mathematical	MulEquiv.trans MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike	left SemidirectProduct instMul MulEquiv.symm congr	—	—
congr_symm_apply_right 📖	mathematical	MulEquiv.trans MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike	right SemidirectProduct instMul MulEquiv.symm congr	—	—
equivProd_apply 📖	mathematical	—	DFunLike.coe Equiv SemidirectProduct EquivLike.toFunLike Equiv.instEquivLike equivProd left right	—	—
equivProd_symm_apply_left 📖	mathematical	—	left DFunLike.coe Equiv SemidirectProduct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivProd	—	—
equivProd_symm_apply_right 📖	mathematical	—	right DFunLike.coe Equiv SemidirectProduct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivProd	—	—
ext 📖	—	left right	—	—	—
ext_iff 📖	mathematical	—	left right	—	ext
hom_ext 📖	—	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup inl inr	—	—	lift_unique lift.congr_simp
inl_aut 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulAut MulAut.instGroup instMul inr InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	ext map_inv MonoidHom.instMonoidHomClass one_mul mul_one inv_one MulAut.inv_apply map_one MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass mul_inv_cancel
inl_aut_inv 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulAut InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulAut.instGroup instMul inr	—	map_inv MonoidHom.instMonoidHomClass inl_aut inv_inv
inl_inj 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl	—	inl_injective
inl_injective 📖	mathematical	—	SemidirectProduct DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl	—	Function.injective_iff_hasLeftInverse One.instNonempty left_inl
inl_left_mul_inr_right 📖	mathematical	—	SemidirectProduct instMul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl left inr right	—	ext map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one one_mul
inr_inj 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inr	—	inr_injective
inr_injective 📖	mathematical	—	SemidirectProduct DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inr	—	Function.injective_iff_hasLeftInverse One.instNonempty right_inr
inv_left 📖	mathematical	—	left SemidirectProduct instInv DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid right	—	—
inv_right 📖	mathematical	—	right SemidirectProduct instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
left_inl 📖	mathematical	—	left DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl	—	—
left_inr 📖	mathematical	—	left DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inr InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
lift_comp_inl 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike MulAut.conj	SemidirectProduct instGroup lift inl	—	MonoidHom.ext lift_inl
lift_comp_inr 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike MulAut.conj	SemidirectProduct instGroup lift inr	—	MonoidHom.ext lift_inr
lift_inl 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike MulAut.conj	SemidirectProduct instGroup lift inl	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one
lift_inr 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike MulAut.conj	SemidirectProduct instGroup lift inr	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul
lift_unique 📖	mathematical	—	lift MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup inl inr	—	DFunLike.ext_iff MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass inl_left_mul_inr_right
map_comp_inl 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	SemidirectProduct instGroup map inl	—	MonoidHom.ext ext map_inl
map_comp_inr 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	SemidirectProduct instGroup map inr	—	MonoidHom.ext ext mk_eq_inl_mul_inr map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul
map_inl 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	SemidirectProduct instGroup map inl	—	mk_eq_inl_mul_inr map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one
map_inr 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	SemidirectProduct instGroup map inr	—	mk_eq_inl_mul_inr map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul
map_left 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	left SemidirectProduct instGroup map	—	—
map_right 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	right SemidirectProduct instGroup map	—	—
mk_eq_inl_mul_inr 📖	mathematical	—	SemidirectProduct instMul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl inr	—	ext map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one one_mul
monoidHomSubgroup_apply 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.normalizer	DFunLike.coe MonoidHom SemidirectProduct SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp MulAut Subgroup.mul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup Subgroup.normalizerMonoidHom Subgroup.inclusion instGroup MonoidHom.instFunLike monoidHomSubgroup MulOne.toMul left right	—	—
mulEquivProd_apply 📖	mathematical	—	DFunLike.coe MulEquiv SemidirectProduct MonoidHom MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup instOneMonoidHom instMul Prod.instMul EquivLike.toFunLike MulEquiv.instEquivLike mulEquivProd left right	—	—
mulEquivProd_symm_apply_left 📖	mathematical	—	left MonoidHom MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup instOneMonoidHom DFunLike.coe MulEquiv SemidirectProduct Prod.instMul instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivProd	—	—
mulEquivProd_symm_apply_right 📖	mathematical	—	right MonoidHom MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup instOneMonoidHom DFunLike.coe MulEquiv SemidirectProduct Prod.instMul instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivProd	—	—
mulEquivSubgroup_apply 📖	mathematical	Subgroup.IsComplement'	DFunLike.coe MulEquiv SemidirectProduct Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp Subgroup.normalizer MulAut Subgroup.mul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup Subgroup.normalizerMonoidHom Subgroup.inclusion Top.top Subgroup.instTop Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder le_top BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subgroup.instCompleteLattice Subgroup.normalizer_eq_top instMul MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike mulEquivSubgroup left right	—	le_top Subgroup.normalizer_eq_top
mulEquivSubgroup_symm_apply 📖	mathematical	Subgroup.IsComplement'	DFunLike.coe MulEquiv SemidirectProduct Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp Subgroup.normalizer MulAut Subgroup.mul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup Subgroup.normalizerMonoidHom Subgroup.inclusion Top.top Subgroup.instTop Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder le_top BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subgroup.instCompleteLattice Subgroup.normalizer_eq_top MulOne.toMul instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivSubgroup Function.surjInv MonoidHom instGroup MonoidHom.instFunLike monoidHomSubgroup Function.Bijective.surjective	—	le_top Subgroup.normalizer_eq_top
mul_def 📖	mathematical	—	SemidirectProduct instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid left DFunLike.coe MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike right	—	—
mul_left 📖	mathematical	—	left SemidirectProduct instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike right	—	—
mul_right 📖	mathematical	—	right SemidirectProduct instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
one_left 📖	mathematical	—	left SemidirectProduct instOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
one_right 📖	mathematical	—	right SemidirectProduct instOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
range_inl_eq_ker_rightHom 📖	mathematical	—	MonoidHom.range SemidirectProduct instGroup inl MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid rightHom	—	le_antisymm ext
rightHom_comp_inl 📖	mathematical	—	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup rightHom inl MonoidHom instOneMonoidHom	—	MonoidHom.ext
rightHom_comp_inr 📖	mathematical	—	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup rightHom inr MonoidHom.id	—	MonoidHom.ext
rightHom_comp_map 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulEquiv.toMonoidHom DFunLike.coe MonoidHom MulAut MulOne.toMul MulAut.instGroup MonoidHom.instFunLike	SemidirectProduct instGroup rightHom map	—	—
rightHom_eq_right 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike rightHom right	—	—
rightHom_inl 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike rightHom inl InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
rightHom_inr 📖	mathematical	—	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike rightHom inr	—	—
rightHom_surjective 📖	mathematical	—	SemidirectProduct DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike rightHom	—	Function.surjective_iff_hasRightInverse rightHom_inr
right_inl 📖	mathematical	—	right DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inl InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
right_inr 📖	mathematical	—	right DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike inr	—	—

(root)

Definitions

Name	Category	Theorems
SemidirectProduct 📖	CompData	61 math math: SemidirectProduct.rightHom_inl, SemidirectProduct.congr_symm_apply_left, SemidirectProduct.one_left, SemidirectProduct.inl_aut, SemidirectProduct.inr_injective, SemidirectProduct.inr_inj, SemidirectProduct.inl_left_mul_inr_right, SemidirectProduct.lift_inr, SemidirectProduct.congr'_apply_right, SemidirectProduct.card, SemidirectProduct.map_comp_inl, SemidirectProduct.rightHom_comp_inr, SemidirectProduct.congr'_apply_left, SemidirectProduct.congr'_symm_apply_right, SemidirectProduct.mul_def, SemidirectProduct.one_right, SemidirectProduct.rightHom_surjective, SemidirectProduct.left_inl, SemidirectProduct.inl_aut_inv, SemidirectProduct.mulEquivProd_symm_apply_left, SemidirectProduct.right_inr, SemidirectProduct.lift_inl, CategoryTheory.ActionCategory.curry_apply_left, SemidirectProduct.equivProd_apply, SemidirectProduct.lift_comp_inl, SemidirectProduct.rightHom_eq_right, SemidirectProduct.congr_symm_apply_right, SemidirectProduct.map_left, SemidirectProduct.congr'_symm_apply_left, SemidirectProduct.rightHom_inr, SemidirectProduct.map_inl, SemidirectProduct.congr_apply_left, SemidirectProduct.map_inr, SemidirectProduct.rightHom_comp_inl, SemidirectProduct.lift_comp_inr, SemidirectProduct.congr_apply_right, SemidirectProduct.inl_inj, SemidirectProduct.map_right, SemidirectProduct.inv_left, SemidirectProduct.mulEquivSubgroup_apply, SemidirectProduct.mul_right, SemidirectProduct.inv_right, SemidirectProduct.mulEquivProd_apply, SemidirectProduct.toGroupExtension_inl, SemidirectProduct.mulEquivSubgroup_symm_apply, SemidirectProduct.lift_unique, SemidirectProduct.mulEquivProd_symm_apply_right, CategoryTheory.ActionCategory.curry_apply_right, SemidirectProduct.map_comp_inr, SemidirectProduct.range_inl_eq_ker_rightHom, SemidirectProduct.right_inl, SemidirectProduct.toGroupExtension_rightHom, SemidirectProduct.mul_left, SemidirectProduct.mk_eq_inl_mul_inr, SemidirectProduct.right_splitting, SemidirectProduct.left_inr, SemidirectProduct.equivProd_symm_apply_left, SemidirectProduct.inl_injective, SemidirectProduct.rightHom_comp_map, SemidirectProduct.monoidHomSubgroup_apply, SemidirectProduct.equivProd_symm_apply_right
instDecidableEqSemidirectProduct 📖	CompOp	—
«term_⋊[_]_» 📖	CompOp	—

instDecidableEqSemidirectProduct

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index