Goursat

📁 Source: Mathlib/GroupTheory/Goursat.lean

Statistics

Metric	Count
Definitions goursatFst, goursatSnd, goursatFst, goursatSnd	4
Theorems goursat, goursatFst_prod_goursatSnd_le, goursat_surjective, mem_goursatFst, mem_goursatSnd, mk_goursatFst_eq_iff_mk_goursatSnd_eq, normal_goursatFst, normal_goursatSnd, goursat, goursatFst_prod_goursatSnd_le, goursat_surjective, mem_goursatFst, mem_goursatSnd, mk_goursatFst_eq_iff_mk_goursatSnd_eq, normal_goursatFst, normal_goursatSnd	16
Total	20

AddSubgroup

Definitions

Name	Category	Theorems
goursatFst 📖	CompOp	6 math math: normal_goursatFst, goursat_surjective, mem_goursatFst, mk_goursatFst_eq_iff_mk_goursatSnd_eq, Submodule.goursatFst_toAddSubgroup, goursatFst_prod_goursatSnd_le
goursatSnd 📖	CompOp	6 math math: normal_goursatSnd, goursat_surjective, Submodule.goursatSnd_toAddSubgroup, mk_goursatFst_eq_iff_mk_goursatSnd_eq, goursatFst_prod_goursatSnd_le, mem_goursatSnd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
goursat 📖	mathematical	—	map AddSubgroup SetLike.instMembership instSetLike Prod.instAddGroup toAddGroup AddMonoidHom.prodMap AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid subtype comap HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addGroup QuotientAddGroup.mk' AddMonoidHom.graph AddEquiv.toAddMonoidHom	—	AddMonoidHom.range_eq_top AddMonoidHom.range_comp range_subtype AddMonoidHom.fst_comp_prod AddMonoidHom.addSubgroupMap_surjective normal_goursatFst normal_goursatSnd goursat_surjective comap_map_eq_self ext AddMonoidHom.mem_ker mem_prod QuotientAddGroup.ker_mk' goursatFst_prod_goursatSnd_le mem_map AddMonoidHom.mem_range
goursatFst_prod_goursatSnd_le 📖	mathematical	—	AddSubgroup Prod.instAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder prod goursatFst goursatSnd	—	add_zero zero_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass mem_goursatFst mem_goursatSnd
goursat_surjective 📖	mathematical	AddSubgroup Prod.instAddGroup SetLike.instMembership instSetLike DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddMonoidHom.instFunLike subtype	AddMonoidHom.range HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup goursatFst goursatSnd QuotientAddGroup.Quotient.addGroup normal_goursatFst normal_goursatSnd AddMonoidHom.comp Prod.instAddZeroClass AddMonoidHom.prodMap QuotientAddGroup.mk' AddMonoidHom.graph AddEquiv.toAddMonoidHom	—	normal_goursatFst normal_goursatSnd AddMonoidHom.exists_addEquiv_range_eq_graph QuotientAddGroup.mk'_surjective mk_goursatFst_eq_iff_mk_goursatSnd_eq
mem_goursatFst 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike goursatFst Prod.instAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_map AddMonoidHom.mem_ker
mem_goursatSnd 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike goursatSnd Prod.instAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_map AddMonoidHom.mem_ker
mk_goursatFst_eq_iff_mk_goursatSnd_eq 📖	mathematical	AddSubgroup Prod.instAddGroup SetLike.instMembership instSetLike DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddMonoidHom.instFunLike subtype	goursatFst goursatSnd	—	normal_goursatFst normal_goursatSnd QuotientAddGroup.eq_iff_sub_mem mem_goursatFst mem_goursatSnd sub_add_cancel zero_add sub_self sub_mem instAddSubgroupClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubgroupClass.toAddSubmonoidClass
normal_goursatFst 📖	mathematical	AddSubgroup Prod.instAddGroup SetLike.instMembership instSetLike DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddMonoidHom.instFunLike subtype	Normal goursatFst	—	Normal.map AddMonoidHom.normal_ker
normal_goursatSnd 📖	mathematical	AddSubgroup Prod.instAddGroup SetLike.instMembership instSetLike DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddMonoidHom.instFunLike subtype	Normal goursatSnd	—	Normal.map AddMonoidHom.normal_ker

Subgroup

Definitions

Name	Category	Theorems
goursatFst 📖	CompOp	5 math math: normal_goursatFst, mem_goursatFst, mk_goursatFst_eq_iff_mk_goursatSnd_eq, goursat_surjective, goursatFst_prod_goursatSnd_le
goursatSnd 📖	CompOp	5 math math: normal_goursatSnd, mk_goursatFst_eq_iff_mk_goursatSnd_eq, mem_goursatSnd, goursat_surjective, goursatFst_prod_goursatSnd_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
goursat 📖	mathematical	—	map Subgroup SetLike.instMembership instSetLike Prod.instGroup toGroup MonoidHom.prodMap Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid subtype comap HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group QuotientGroup.mk' MonoidHom.graph MulEquiv.toMonoidHom	—	MonoidHom.range_comp range_subtype MonoidHom.fst_comp_prod MonoidHom.subgroupMap_surjective normal_goursatFst normal_goursatSnd goursat_surjective comap_map_eq_self ext QuotientGroup.ker_mk' goursatFst_prod_goursatSnd_le
goursatFst_prod_goursatSnd_le 📖	mathematical	—	Subgroup Prod.instGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder prod goursatFst goursatSnd	—	mul_one one_mul MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass instSubgroupClass mem_goursatFst mem_goursatSnd
goursat_surjective 📖	mathematical	Subgroup Prod.instGroup SetLike.instMembership instSetLike DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MonoidHom.instFunLike subtype	MonoidHom.range HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup goursatFst goursatSnd QuotientGroup.Quotient.group normal_goursatFst normal_goursatSnd MonoidHom.comp Prod.instMulOneClass MonoidHom.prodMap QuotientGroup.mk' MonoidHom.graph MulEquiv.toMonoidHom	—	normal_goursatFst normal_goursatSnd MonoidHom.exists_mulEquiv_range_eq_graph QuotientGroup.mk'_surjective mk_goursatFst_eq_iff_mk_goursatSnd_eq
mem_goursatFst 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike goursatFst Prod.instGroup InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mem_goursatSnd 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike goursatSnd Prod.instGroup InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mk_goursatFst_eq_iff_mk_goursatSnd_eq 📖	mathematical	Subgroup Prod.instGroup SetLike.instMembership instSetLike DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MonoidHom.instFunLike subtype	goursatFst goursatSnd	—	normal_goursatFst normal_goursatSnd div_mul_cancel one_mul div_self' div_mem instSubgroupClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass
normal_goursatFst 📖	mathematical	Subgroup Prod.instGroup SetLike.instMembership instSetLike DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MonoidHom.instFunLike subtype	Normal goursatFst	—	Normal.map MonoidHom.normal_ker
normal_goursatSnd 📖	mathematical	Subgroup Prod.instGroup SetLike.instMembership instSetLike DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MonoidHom.instFunLike subtype	Normal goursatSnd	—	Normal.map MonoidHom.normal_ker

---

← Back to Index