Basic

📁 Source: Mathlib/GroupTheory/GroupExtension/Basic.lean

Statistics

Metric	Count
Definitions ConjClasses, ofAddMonoidHom, setoid, equivComp, quotientKerRightHomEquivRight, quotientRangeInlEquivRight, surjInvRightHom, ConjClasses, ofMonoidHom, setoid, equivComp, conjAct, semidirectProductMulEquiv, semidirectProductToGroupExtensionEquiv, quotientKerRightHomEquivRight, quotientRangeInlEquivRight, surjInvRightHom	17
Theorems refl, trans, add_add_add_neg_mem_range_inl, add_neg_add_add_mem_range_inl, add_neg_mem_range_inl, equivComp_apply, exists_add_eq_add_add_inl, exists_add_eq_inl_add_add, exists_eq_add_inl, exists_eq_inl_add, neg_add_mem_range_inl, refl, trans, equivComp_apply, exists_eq_inl_mul, exists_eq_mul_inl, exists_mul_eq_inl_mul_mul, exists_mul_eq_mul_mul_inl, inv_mul_mem_range_inl, mul_inv_mem_range_inl, mul_inv_mul_mul_mem_range_inl, mul_mul_mul_inv_mem_range_inl, right_splitting	23
Total	40

AddGroupExtension

Definitions

Name	Category	Theorems
ConjClasses 📖	CompOp	—
quotientKerRightHomEquivRight 📖	CompOp	—
quotientRangeInlEquivRight 📖	CompOp	—
surjInvRightHom 📖	CompOp	—

AddGroupExtension.Equiv

Definitions

Name	Category	Theorems
ofAddMonoidHom 📖	CompOp	—

AddGroupExtension.IsConj

Definitions

Name	Category	Theorems
setoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	mathematical	—	AddGroupExtension.IsConj	—	map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass zero_add neg_zero add_zero
trans 📖	—	AddGroupExtension.IsConj	—	—	map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass neg_one_zsmul add_assoc neg_one_zsmul_add

AddGroupExtension.Section

Definitions

Name	Category	Theorems
equivComp 📖	CompOp	1 math math: equivComp_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_add_add_neg_mem_range_inl 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range AddGroupExtension.inl AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DFunLike.coe AddGroupExtension.Section instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	AddGroupExtension.range_inl_eq_ker_rightHom AddMonoidHom.mem_ker map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass rightHom_section map_neg add_neg_cancel
add_neg_add_add_mem_range_inl 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range AddGroupExtension.inl AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFunLike.coe AddGroupExtension.Section instFunLike	—	AddGroupExtension.range_inl_eq_ker_rightHom add_assoc AddMonoidHom.mem_ker map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass map_neg rightHom_section neg_add_cancel
add_neg_mem_range_inl 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range AddGroupExtension.inl AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DFunLike.coe AddGroupExtension.Section instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	AddGroupExtension.range_inl_eq_ker_rightHom AddMonoidHom.mem_ker map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass rightHom_section map_neg add_neg_cancel
equivComp_apply 📖	mathematical	—	DFunLike.coe AddGroupExtension.Section instFunLike equivComp AddGroupExtension.Equiv EquivLike.toFunLike AddGroupExtension.Equiv.instEquivLike	—	—
exists_add_eq_add_add_inl 📖	mathematical	—	DFunLike.coe AddGroupExtension.Section instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom AddMonoidHom.instFunLike AddGroupExtension.inl	—	add_neg_add_add_mem_range_inl map_neg AddMonoidHom.instAddMonoidHomClass eq_add_neg_iff_add_eq eq_neg_add_iff_add_eq add_assoc
exists_add_eq_inl_add_add 📖	mathematical	—	DFunLike.coe AddGroupExtension.Section instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom AddMonoidHom.instFunLike AddGroupExtension.inl	—	add_add_add_neg_mem_range_inl add_assoc map_neg AddMonoidHom.instAddMonoidHomClass eq_neg_add_iff_add_eq eq_add_neg_iff_add_eq
exists_eq_add_inl 📖	mathematical	—	DFunLike.coe AddGroupExtension.Section instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom AddMonoidHom.instFunLike AddGroupExtension.inl	—	neg_add_mem_range_inl add_neg_cancel_left
exists_eq_inl_add 📖	mathematical	—	DFunLike.coe AddGroupExtension.Section instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom AddMonoidHom.instFunLike AddGroupExtension.inl	—	add_neg_mem_range_inl neg_add_cancel_right
neg_add_mem_range_inl 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range AddGroupExtension.inl AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFunLike.coe AddGroupExtension.Section instFunLike	—	AddGroupExtension.range_inl_eq_ker_rightHom AddMonoidHom.mem_ker map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass map_neg rightHom_section neg_add_cancel

GroupExtension

Definitions

Name	Category	Theorems
ConjClasses 📖	CompOp	—
quotientKerRightHomEquivRight 📖	CompOp	—
quotientRangeInlEquivRight 📖	CompOp	—
surjInvRightHom 📖	CompOp	—

GroupExtension.Equiv

Definitions

Name	Category	Theorems
ofMonoidHom 📖	CompOp	—

GroupExtension.IsConj

Definitions

Name	Category	Theorems
setoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	mathematical	—	GroupExtension.IsConj	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul inv_one mul_one
trans 📖	—	GroupExtension.IsConj	—	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_zpow_neg_one

GroupExtension.Section

Definitions

Name	Category	Theorems
equivComp 📖	CompOp	1 math math: equivComp_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivComp_apply 📖	mathematical	—	DFunLike.coe GroupExtension.Section instFunLike equivComp GroupExtension.Equiv EquivLike.toFunLike GroupExtension.Equiv.instEquivLike	—	—
exists_eq_inl_mul 📖	mathematical	—	DFunLike.coe GroupExtension.Section instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom MonoidHom.instFunLike GroupExtension.inl	—	mul_inv_mem_range_inl inv_mul_cancel_right
exists_eq_mul_inl 📖	mathematical	—	DFunLike.coe GroupExtension.Section instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom MonoidHom.instFunLike GroupExtension.inl	—	inv_mul_mem_range_inl mul_inv_cancel_left
exists_mul_eq_inl_mul_mul 📖	mathematical	—	DFunLike.coe GroupExtension.Section instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom MonoidHom.instFunLike GroupExtension.inl	—	mul_mul_mul_inv_mem_range_inl mul_assoc map_inv MonoidHom.instMonoidHomClass eq_inv_mul_iff_mul_eq eq_mul_inv_iff_mul_eq
exists_mul_eq_mul_mul_inl 📖	mathematical	—	DFunLike.coe GroupExtension.Section instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom MonoidHom.instFunLike GroupExtension.inl	—	mul_inv_mul_mul_mem_range_inl map_inv MonoidHom.instMonoidHomClass eq_mul_inv_iff_mul_eq eq_inv_mul_iff_mul_eq mul_assoc
inv_mul_mem_range_inl 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range GroupExtension.inl MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe GroupExtension.Section instFunLike	—	GroupExtension.range_inl_eq_ker_rightHom map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv rightHom_section inv_mul_cancel
mul_inv_mem_range_inl 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range GroupExtension.inl MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe GroupExtension.Section instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	GroupExtension.range_inl_eq_ker_rightHom map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass rightHom_section map_inv mul_inv_cancel
mul_inv_mul_mul_mem_range_inl 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range GroupExtension.inl MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe GroupExtension.Section instFunLike	—	GroupExtension.range_inl_eq_ker_rightHom mul_assoc map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv rightHom_section inv_mul_cancel
mul_mul_mul_inv_mem_range_inl 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range GroupExtension.inl MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe GroupExtension.Section instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	GroupExtension.range_inl_eq_ker_rightHom map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass rightHom_section map_inv mul_inv_cancel

GroupExtension.Splitting

Definitions

Name	Category	Theorems
conjAct 📖	CompOp	—
semidirectProductMulEquiv 📖	CompOp	—
semidirectProductToGroupExtensionEquiv 📖	CompOp	—

SemidirectProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
right_splitting 📖	mathematical	—	right DFunLike.coe GroupExtension.Splitting SemidirectProduct instGroup toGroupExtension GroupExtension.Splitting.instFunLike	—	rightHom_eq_right toGroupExtension_rightHom GroupExtension.Splitting.rightHom_splitting

---

← Back to Index