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	39 math math: rightHom_inl, inl_aut, inr_injective, inr_inj, inl_left_mul_inr_right, lift_inr, CategoryTheory.ActionCategory.uncurry_map, 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	21 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, isZGroup_iff_exists_mulEquiv, 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 DFunLike.coe MulEquiv SemidirectProduct instMul EquivLike.toFunLike MulEquiv.instEquivLike congr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
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 DFunLike.coe MulEquiv SemidirectProduct instMul EquivLike.toFunLike MulEquiv.instEquivLike congr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
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 DFunLike.coe MulEquiv SemidirectProduct instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm congr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
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 DFunLike.coe MulEquiv SemidirectProduct instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm congr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
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	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid 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	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid 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	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike 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	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike 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	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid 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	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid 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	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike 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	DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike 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 DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike 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 DFunLike.coe MonoidHom SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike 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 SetLike.coe Subgroup.instSetLike	DFunLike.coe MonoidHom SemidirectProduct Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp Subgroup.normalizer SetLike.coe 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 SetLike.coe 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 SetLike.coe 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	MonoidHom.comp SemidirectProduct MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid 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	63 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, CategoryTheory.ActionCategory.uncurry_map, 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, isZGroup_iff_exists_mulEquiv, 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