Basic

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

Statistics

Metric	Count
Definitions `addAction`, `addSubmonoid`, `comapQuotientEquiv`, `comapQuotientEquivOfSurj`, `instVAdd`, `ofAddSubmonoid`, `pi`, `prod`, `quotientKerEquivOfRightInverse`, `quotientKerEquivOfSurjective`, `quotientKerEquivRange`, `quotientQuotientEquivQuotient`, `toAddSubmonoid`, `comapQuotientEquiv`, `comapQuotientEquivOfSurj`, `instSMul`, `mulAction`, `mulDistribMulAction`, `ofSubmonoid`, `pi`, `prod`, `quotientKerEquivOfRightInverse`, `quotientKerEquivOfSurjective`, `quotientKerEquivRange`, `quotientQuotientEquivQuotient`, `submonoid`, `toSubmonoid`	27
Theorems `coe_vadd`, `comapQuotientEquivOfSurj_mk`, `comapQuotientEquivOfSurj_symm_mk`, `comapQuotientEquivOfSurj_symm_mk'`, `comap_conGen_equiv`, `comap_conGen_of_bijective`, `congr_mk`, `kerLift_range_eq`, `le_comap_conGen`, `le_iff`, `lift_range`, `mem_coe`, `mrange_mk'`, `quotientKerEquivOfRightInverse_apply`, `quotientKerEquivOfRightInverse_symm_apply`, `to_addSubmonoid_inj`, `vadd`, `coe_smul`, `comapQuotientEquivOfSurj_mk`, `comapQuotientEquivOfSurj_symm_mk`, `comapQuotientEquivOfSurj_symm_mk'`, `comap_conGen_equiv`, `comap_conGen_of_bijective`, `congr_mk`, `instIsCentralScalar`, `instIsScalarTower`, `instSMulCommClass`, `kerLift_range_eq`, `le_comap_conGen`, `le_iff`, `lift_range`, `mem_coe`, `mrange_mk'`, `quotientKerEquivOfRightInverse_apply`, `quotientKerEquivOfRightInverse_symm_apply`, `smul`, `to_submonoid_inj`	37
Total	64

AddCon

Definitions

Name	Category	Theorems
`addAction` 📖	CompOp	—
`addSubmonoid` 📖	CompOp	2 math math: `le_iff`, `mem_coe`
`comapQuotientEquiv` 📖	CompOp	—
`comapQuotientEquivOfSurj` 📖	CompOp	3 math math: `comapQuotientEquivOfSurj_symm_mk`, `comapQuotientEquivOfSurj_symm_mk'`, `comapQuotientEquivOfSurj_mk`
`instVAdd` 📖	CompOp	1 math math: `coe_vadd`
`ofAddSubmonoid` 📖	CompOp	—
`pi` 📖	CompOp	—
`prod` 📖	CompOp	—
`quotientKerEquivOfRightInverse` 📖	CompOp	2 math math: `quotientKerEquivOfRightInverse_apply`, `quotientKerEquivOfRightInverse_symm_apply`
`quotientKerEquivOfSurjective` 📖	CompOp	—
`quotientKerEquivRange` 📖	CompOp	—
`quotientQuotientEquivQuotient` 📖	CompOp	—
`toAddSubmonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_vadd` 📖	mathematical	—	`toQuotient` `AddZero.toAdd` `AddZeroClass.toAddZero` `HVAdd.hVAdd` `instHVAdd` `Quotient` `instVAdd`	—	—
`comapQuotientEquivOfSurj_mk` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddEquiv` `Quotient` `AddZero.toAdd` `comap` `AddMonoidHom.map_add` `hasAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `comapQuotientEquivOfSurj` `toQuotient`	—	`AddMonoidHom.map_add`
`comapQuotientEquivOfSurj_symm_mk` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddEquiv` `Quotient` `AddZero.toAdd` `comap` `AddMonoidHom.map_add` `hasAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `comapQuotientEquivOfSurj` `toQuotient`	—	`AddMonoidHom.map_add` `AddEquiv.symm_apply_eq`
`comapQuotientEquivOfSurj_symm_mk'` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Quotient` `AddZero.toAdd` `AddZeroClass.toAddZero` `comap` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddMonoidHom.map_add` `AddMonoidHomClass.toAddMonoidHom` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `hasAdd` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddEquiv.symm` `comapQuotientEquivOfSurj` `AddEquiv.surjective` `toSetoid` `toQuotient`	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddMonoidHom.map_add` `AddEquiv.surjective` `AddEquiv.symm_apply_eq`
`comap_conGen_equiv` 📖	mathematical	—	`comap` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `map_add` `AddEquivClass.instAddHomClass` `AddEquiv.instAddEquivClass` `addConGen`	—	`le_antisymm` `map_add` `AddEquivClass.instAddHomClass` `AddEquiv.instAddEquivClass` `AddEquiv.injective` `AddEquiv.surjective` `AddEquiv.eq_symm_apply` `AddEquiv.apply_symm_apply` `comap_rel` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv` `le_comap_conGen`
`comap_conGen_of_bijective` 📖	mathematical	`Function.Bijective`	`comap` `addConGen`	—	`comap_conGen_equiv` `AddHom.addHomClass`
`congr_mk` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Quotient` `hasAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `congr` `toQuotient`	—	—
`kerLift_range_eq` 📖	mathematical	—	`AddMonoidHom.mrange` `Quotient` `AddZero.toAdd` `AddZeroClass.toAddZero` `ker` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `addZeroClass` `kerLift`	—	`lift_range` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`
`le_comap_conGen` 📖	mathematical	—	`AddCon` `instLE` `addConGen` `comap`	—	`comap_rel`
`le_iff` 📖	mathematical	—	`AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `instLE` `AddSubmonoid` `Prod.instAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubmonoid.instPartialOrder` `addSubmonoid`	—	—
`lift_range` 📖	mathematical	`AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `instLE` `ker` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`	`AddMonoidHom.mrange` `Quotient` `addZeroClass` `lift`	—	`AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.ext`
`mem_coe` 📖	mathematical	—	`AddSubmonoid` `Prod.instAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `addSubmonoid` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `instMembershipProd`	—	—
`mrange_mk'` 📖	mathematical	—	`AddMonoidHom.mrange` `Quotient` `AddZero.toAdd` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `mk'` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop`	—	`AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.mrange_eq_top` `mk'_surjective`
`quotientKerEquivOfRightInverse_apply` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddEquiv` `Quotient` `AddZero.toAdd` `ker` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `hasAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `quotientKerEquivOfRightInverse` `addZeroClass` `kerLift`	—	`AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`
`quotientKerEquivOfRightInverse_symm_apply` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddEquiv` `Quotient` `AddZero.toAdd` `ker` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `hasAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `quotientKerEquivOfRightInverse` `toQuotient`	—	`AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`
`to_addSubmonoid_inj` 📖	—	`addSubmonoid`	—	—	`ext`
`vadd` 📖	mathematical	`DFunLike.coe` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `instFunLikeForallProp`	`HVAdd.hVAdd` `instHVAdd`	—	`vadd_zero_add` `add` `Setoid.refl'`

Con

Definitions

Name	Category	Theorems
`comapQuotientEquiv` 📖	CompOp	—
`comapQuotientEquivOfSurj` 📖	CompOp	3 math math: `comapQuotientEquivOfSurj_symm_mk'`, `comapQuotientEquivOfSurj_mk`, `comapQuotientEquivOfSurj_symm_mk`
`instSMul` 📖	CompOp	4 math math: `instIsScalarTower`, `instSMulCommClass`, `coe_smul`, `instIsCentralScalar`
`mulAction` 📖	CompOp	—
`mulDistribMulAction` 📖	CompOp	—
`ofSubmonoid` 📖	CompOp	—
`pi` 📖	CompOp	—
`prod` 📖	CompOp	—
`quotientKerEquivOfRightInverse` 📖	CompOp	2 math math: `quotientKerEquivOfRightInverse_symm_apply`, `quotientKerEquivOfRightInverse_apply`
`quotientKerEquivOfSurjective` 📖	CompOp	—
`quotientKerEquivRange` 📖	CompOp	—
`quotientQuotientEquivQuotient` 📖	CompOp	—
`submonoid` 📖	CompOp	2 math math: `le_iff`, `mem_coe`
`toSubmonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`toQuotient` `MulOne.toMul` `MulOneClass.toMulOne` `Quotient` `instSMul`	—	—
`comapQuotientEquivOfSurj_mk` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MulEquiv` `Quotient` `MulOne.toMul` `comap` `MonoidHom.map_mul` `hasMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `comapQuotientEquivOfSurj` `toQuotient`	—	`MonoidHom.map_mul`
`comapQuotientEquivOfSurj_symm_mk` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MulEquiv` `Quotient` `MulOne.toMul` `comap` `MonoidHom.map_mul` `hasMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `comapQuotientEquivOfSurj` `toQuotient`	—	`MonoidHom.map_mul` `MulEquiv.symm_apply_eq`
`comapQuotientEquivOfSurj_symm_mk'` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `comap` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MonoidHom.map_mul` `MonoidHomClass.toMonoidHom` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `hasMul` `MonoidHom` `MonoidHom.instFunLike` `MulEquiv.symm` `comapQuotientEquivOfSurj` `MulEquiv.surjective` `toSetoid` `toQuotient`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MonoidHom.map_mul` `MulEquiv.surjective` `MulEquiv.symm_apply_eq`
`comap_conGen_equiv` 📖	mathematical	—	`comap` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `map_mul` `MulEquivClass.instMulHomClass` `MulEquiv.instMulEquivClass` `conGen`	—	`le_antisymm` `map_mul` `MulEquivClass.instMulHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.injective` `MulEquiv.surjective` `MulEquiv.eq_symm_apply` `MulEquiv.apply_symm_apply` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv` `le_comap_conGen`
`comap_conGen_of_bijective` 📖	mathematical	`Function.Bijective`	`comap` `conGen`	—	`comap_conGen_equiv` `MulHom.mulHomClass`
`congr_mk` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Quotient` `hasMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `congr` `toQuotient`	—	—
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMul` `MulOpposite`	—	`Quotient.ind'` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMul`	—	`Quotient.ind'` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMul`	—	`Quotient.ind'` `SMulCommClass.smul_comm`
`kerLift_range_eq` 📖	mathematical	—	`MonoidHom.mrange` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `ker` `MonoidHom` `MonoidHom.instFunLike` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `mulOneClass` `kerLift`	—	`lift_range` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`le_comap_conGen` 📖	mathematical	—	`Con` `instLE` `conGen` `comap`	—	—
`le_iff` 📖	mathematical	—	`Con` `MulOne.toMul` `MulOneClass.toMulOne` `instLE` `Submonoid` `Prod.instMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `submonoid`	—	—
`lift_range` 📖	mathematical	`Con` `MulOne.toMul` `MulOneClass.toMulOne` `instLE` `ker` `MonoidHom` `MonoidHom.instFunLike` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`	`MonoidHom.mrange` `Quotient` `mulOneClass` `lift`	—	`MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Submonoid.ext`
`mem_coe` 📖	mathematical	—	`Submonoid` `Prod.instMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `submonoid` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `instMembershipProd`	—	—
`mrange_mk'` 📖	mathematical	—	`MonoidHom.mrange` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `mk'` `Top.top` `Submonoid` `Submonoid.instTop`	—	`MonoidHom.instMonoidHomClass` `MonoidHom.mrange_eq_top` `mk'_surjective`
`quotientKerEquivOfRightInverse_apply` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MulEquiv` `Quotient` `MulOne.toMul` `ker` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `hasMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `quotientKerEquivOfRightInverse` `mulOneClass` `kerLift`	—	`MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`quotientKerEquivOfRightInverse_symm_apply` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MulEquiv` `Quotient` `MulOne.toMul` `ker` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `hasMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `quotientKerEquivOfRightInverse` `toQuotient`	—	`MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`smul` 📖	—	`DFunLike.coe` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `instFunLikeForallProp`	—	—	`smul_one_mul` `mul` `Setoid.refl'`
`to_submonoid_inj` 📖	—	`submonoid`	—	—	`ext`

---

← Back to Index