Hom

📁 Source: Mathlib/GroupTheory/Congruence/Hom.lean

Statistics

Metric	Count
Definitions correspondence, ker, kerLift, map, mapGen, mapOfSurjective, mk', mkAddHom, correspondence, ker, kerLift, map, mapGen, mapOfSurjective, mk', mkMulHom	16
Theorems coe_mk', comap_eq, hom_ext, hom_ext_iff, kerLift_injective, kerLift_mk, ker_apply, ker_coeAddHom, ker_eq_lift_of_injective, ker_mkAddHom_eq, ker_rel, lift_apply_mk', lift_coe, lift_comp_mk', lift_funext, lift_mk', lift_surjective_of_surjective, lift_unique, mapOfSurjective_eq_mapGen, map_apply, mk'_ker, mk'_surjective, mkAddHom_apply, coe_mk', comap_eq, hom_ext, hom_ext_iff, kerLift_injective, kerLift_mk, ker_apply, ker_coeMulHom, ker_eq_lift_of_injective, ker_mkMulHom_eq, ker_rel, lift_apply_mk', lift_coe, lift_comp_mk', lift_funext, lift_mk', lift_surjective_of_surjective, lift_unique, mapOfSurjective_eq_mapGen, map_apply, mk'_ker, mk'_surjective, mkMulHom_apply	46
Total	62

AddCon

Definitions

Name	Category	Theorems
correspondence 📖	CompOp	—
ker 📖	CompOp	13 math math: ker_coeAddHom, ker_mkAddHom_eq, ker_rel, comap_eq, kerLift_range_eq, kerLift_mk, ker_apply, mk'_ker, QuotientAddGroup.con_ker_eq_addConKer, kerLift_injective, quotientKerEquivOfRightInverse_apply, AddMonoid.Coprod.con_ker_mk, quotientKerEquivOfRightInverse_symm_apply
kerLift 📖	CompOp	4 math math: kerLift_range_eq, kerLift_mk, kerLift_injective, quotientKerEquivOfRightInverse_apply
map 📖	CompOp	1 math math: map_apply
mapGen 📖	CompOp	1 math math: mapOfSurjective_eq_mapGen
mapOfSurjective 📖	CompOp	1 math math: mapOfSurjective_eq_mapGen
mk' 📖	CompOp	10 math math: mk'_surjective, hom_ext_iff, lift_comp_mk', mrange_mk', comap_eq, coe_mk', mk'_ker, lift_mk', map_apply, lift_apply_mk'
mkAddHom 📖	CompOp	2 math math: ker_mkAddHom_eq, mkAddHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk' 📖	mathematical	—	DFunLike.coe AddMonoidHom Quotient AddZero.toAdd AddZeroClass.toAddZero addZeroClass AddMonoidHom.instFunLike mk' toQuotient	—	—
comap_eq 📖	mathematical	—	comap AddZero.toAdd AddZeroClass.toAddZero DFunLike.coe AddMonoidHom AddMonoidHom.instFunLike AddMonoidHom.map_add ker Quotient addZeroClass AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass AddMonoidHom.comp mk'	—	ext AddMonoidHom.map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass eq
hom_ext 📖	—	AddMonoidHom.comp Quotient AddZero.toAdd AddZeroClass.toAddZero addZeroClass mk'	—	—	lift_apply_mk' AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
hom_ext_iff 📖	mathematical	—	AddMonoidHom.comp Quotient AddZero.toAdd AddZeroClass.toAddZero addZeroClass mk'	—	hom_ext
kerLift_injective 📖	mathematical	—	Quotient AddZero.toAdd AddZeroClass.toAddZero ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass DFunLike.coe addZeroClass kerLift	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Quotient.inductionOn₂' eq
kerLift_mk 📖	mathematical	—	DFunLike.coe AddMonoidHom Quotient AddZero.toAdd AddZeroClass.toAddZero ker AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass addZeroClass kerLift toQuotient	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
ker_apply 📖	mathematical	—	DFunLike.coe AddCon AddZero.toAdd AddZeroClass.toAddZero instFunLikeForallProp ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
ker_coeAddHom 📖	mathematical	—	ker AddHom AddHom.funLike AddHom.addHomClass AddHomClass.toAddHom	—	AddHom.addHomClass
ker_eq_lift_of_injective 📖	—	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Quotient DFunLike.coe addZeroClass lift	—	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass toSetoid_injective Setoid.ker_eq_lift_of_injective
ker_mkAddHom_eq 📖	mathematical	—	ker Quotient AddHom hasAdd AddHom.funLike AddHom.addHomClass mkAddHom	—	ext AddHom.addHomClass Quotient.eq''
ker_rel 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp ker	—	—
lift_apply_mk' 📖	mathematical	—	lift AddMonoidHom.comp Quotient AddZero.toAdd AddZeroClass.toAddZero addZeroClass mk'	—	AddMonoidHom.ext
lift_coe 📖	mathematical	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass	DFunLike.coe Quotient addZeroClass lift toQuotient	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
lift_comp_mk' 📖	mathematical	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass	AddMonoidHom.comp Quotient addZeroClass lift mk'	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass AddMonoidHom.ext
lift_funext 📖	—	DFunLike.coe AddMonoidHom Quotient AddZero.toAdd AddZeroClass.toAddZero addZeroClass AddMonoidHom.instFunLike toQuotient	—	—	hom_ext DFunLike.ext
lift_mk' 📖	mathematical	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass	DFunLike.coe Quotient addZeroClass lift mk'	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
lift_surjective_of_surjective 📖	mathematical	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass DFunLike.coe	Quotient addZeroClass lift	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass lift_mk'
lift_unique 📖	mathematical	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE ker AddMonoidHom AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass AddMonoidHom.comp Quotient addZeroClass mk'	lift	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass hom_ext
mapOfSurjective_eq_mapGen 📖	mathematical	AddCon instLE ker DFunLike.coe	mapGen mapOfSurjective	—	addConGen_of_addCon
map_apply 📖	mathematical	AddCon AddZero.toAdd AddZeroClass.toAddZero instLE	DFunLike.coe AddMonoidHom Quotient addZeroClass AddMonoidHom.instFunLike map lift mk' toQuotient instFunLikeForallProp eq	—	—
mk'_ker 📖	mathematical	—	ker Quotient AddZero.toAdd AddZeroClass.toAddZero AddMonoidHom addZeroClass AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass mk'	—	ext AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass eq
mk'_surjective 📖	mathematical	—	Quotient AddZero.toAdd AddZeroClass.toAddZero DFunLike.coe AddMonoidHom addZeroClass AddMonoidHom.instFunLike mk'	—	Quotient.mk''_surjective
mkAddHom_apply 📖	mathematical	—	DFunLike.coe AddHom Quotient hasAdd AddHom.funLike mkAddHom toQuotient	—	—

Con

Definitions

Name	Category	Theorems
correspondence 📖	CompOp	—
ker 📖	CompOp	13 math math: Monoid.Coprod.con_ker_mk, ker_rel, ker_apply, kerLift_mk, ker_coeMulHom, quotientKerEquivOfRightInverse_symm_apply, kerLift_range_eq, QuotientGroup.con_ker_eq_conKer, quotientKerEquivOfRightInverse_apply, comap_eq, mk'_ker, kerLift_injective, ker_mkMulHom_eq
kerLift 📖	CompOp	4 math math: kerLift_mk, kerLift_range_eq, quotientKerEquivOfRightInverse_apply, kerLift_injective
map 📖	CompOp	1 math math: map_apply
mapGen 📖	CompOp	1 math math: mapOfSurjective_eq_mapGen
mapOfSurjective 📖	CompOp	1 math math: mapOfSurjective_eq_mapGen
mk' 📖	CompOp	11 math math: hom_ext_iff, mk'_surjective, lift_comp_mk', Monoid.CoprodI.of_apply, comap_eq, coe_mk', lift_mk', lift_apply_mk', mk'_ker, map_apply, mrange_mk'
mkMulHom 📖	CompOp	2 math math: mkMulHom_apply, ker_mkMulHom_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk' 📖	mathematical	—	DFunLike.coe MonoidHom Quotient MulOne.toMul MulOneClass.toMulOne mulOneClass MonoidHom.instFunLike mk' toQuotient	—	—
comap_eq 📖	mathematical	—	comap MulOne.toMul MulOneClass.toMulOne DFunLike.coe MonoidHom MonoidHom.instFunLike MonoidHom.map_mul ker Quotient mulOneClass MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass MonoidHom.comp mk'	—	ext MonoidHom.map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass eq
hom_ext 📖	—	MonoidHom.comp Quotient MulOne.toMul MulOneClass.toMulOne mulOneClass mk'	—	—	lift_apply_mk' MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
hom_ext_iff 📖	mathematical	—	MonoidHom.comp Quotient MulOne.toMul MulOneClass.toMulOne mulOneClass mk'	—	hom_ext
kerLift_injective 📖	mathematical	—	Quotient MulOne.toMul MulOneClass.toMulOne ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass DFunLike.coe mulOneClass kerLift	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Quotient.inductionOn₂' eq
kerLift_mk 📖	mathematical	—	DFunLike.coe MonoidHom Quotient MulOne.toMul MulOneClass.toMulOne ker MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mulOneClass kerLift toQuotient	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
ker_apply 📖	mathematical	—	DFunLike.coe Con MulOne.toMul MulOneClass.toMulOne instFunLikeForallProp ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
ker_coeMulHom 📖	mathematical	—	ker MulHom MulHom.funLike MulHom.mulHomClass MulHomClass.toMulHom	—	MulHom.mulHomClass
ker_eq_lift_of_injective 📖	—	Con MulOne.toMul MulOneClass.toMulOne instLE ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Quotient DFunLike.coe mulOneClass lift	—	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass toSetoid_injective Setoid.ker_eq_lift_of_injective
ker_mkMulHom_eq 📖	mathematical	—	ker Quotient MulHom hasMul MulHom.funLike MulHom.mulHomClass mkMulHom	—	ext MulHom.mulHomClass Quotient.eq''
ker_rel 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp ker	—	—
lift_apply_mk' 📖	mathematical	—	lift MonoidHom.comp Quotient MulOne.toMul MulOneClass.toMulOne mulOneClass mk'	—	MonoidHom.ext
lift_coe 📖	mathematical	Con MulOne.toMul MulOneClass.toMulOne instLE ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass	DFunLike.coe Quotient mulOneClass lift toQuotient	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
lift_comp_mk' 📖	mathematical	Con MulOne.toMul MulOneClass.toMulOne instLE ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass	MonoidHom.comp Quotient mulOneClass lift mk'	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass MonoidHom.ext
lift_funext 📖	—	DFunLike.coe MonoidHom Quotient MulOne.toMul MulOneClass.toMulOne mulOneClass MonoidHom.instFunLike toQuotient	—	—	hom_ext DFunLike.ext
lift_mk' 📖	mathematical	Con MulOne.toMul MulOneClass.toMulOne instLE ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass	DFunLike.coe Quotient mulOneClass lift mk'	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
lift_surjective_of_surjective 📖	mathematical	Con MulOne.toMul MulOneClass.toMulOne instLE ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass DFunLike.coe	Quotient mulOneClass lift	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass lift_mk'
lift_unique 📖	mathematical	Con MulOne.toMul MulOneClass.toMulOne instLE ker MonoidHom MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass MonoidHom.comp Quotient mulOneClass mk'	lift	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass hom_ext
mapOfSurjective_eq_mapGen 📖	mathematical	Con instLE ker DFunLike.coe	mapGen mapOfSurjective	—	conGen_of_con
map_apply 📖	mathematical	Con MulOne.toMul MulOneClass.toMulOne instLE	DFunLike.coe MonoidHom Quotient mulOneClass MonoidHom.instFunLike map lift mk' toQuotient instFunLikeForallProp eq	—	—
mk'_ker 📖	mathematical	—	ker Quotient MulOne.toMul MulOneClass.toMulOne MonoidHom mulOneClass MonoidHom.instFunLike MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mk'	—	ext MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass eq
mk'_surjective 📖	mathematical	—	Quotient MulOne.toMul MulOneClass.toMulOne DFunLike.coe MonoidHom mulOneClass MonoidHom.instFunLike mk'	—	Quotient.mk''_surjective
mkMulHom_apply 📖	mathematical	—	DFunLike.coe MulHom Quotient hasMul MulHom.funLike mkMulHom toQuotient	—	—

---

← Back to Index