| Metric | Count |
|---|
DefinitionsAddCon, inhabited, addCommGroup, addCommMagma, addCommMonoid, addCommSemigroup, addGroup, addMonoid, addSemigroup, addZeroClass, comap, gi, hasAdd, hasNeg, hasSub, hrecOn₂, instCoeTCQuotient, instCompleteLattice, instDecidableEqQuotientOfDecidableCoeForallProp, instFunLikeForallProp, instInfSet, instInhabited, instLE, instMembershipProd, instNSMulQuotientNat, instPartialOrder, instZSMul, liftOn, liftOnAddUnits, liftOn₂, toQuotient, toSetoid, zero, Con, inhabited, comap, commGroup, commMagma, commMonoid, commSemigroup, gi, group, hasDiv, hasInv, hasMul, hrecOn₂, instCoeTCQuotient, instCompleteLattice, instDecidableEqQuotientOfDecidableCoeForallProp, instFunLikeForallProp, instInfSet, instInhabited, instLE, instMembershipProd, instPartialOrder, instPowQuotientNat, instZPow, liftOn, liftOnUnits, liftOn₂, monoid, mulOneClass, one, semigroup, toQuotient, toSetoid, addConGen, conGen | 68 |
Theoremsadd, add', addConGen_eq, addConGen_idem, addConGen_le, addConGen_mono, addConGen_of_addCon, coe_add, coe_iInf, coe_inf, coe_inj, coe_sInf, coe_zero, comap_rel, eq, ext, ext', ext_iff, hrec_on₂_coe, induction_on, induction_on_addUnits, induction_on₂, inf_iff_and, le_def, liftOnAddUnits_mk, liftOn_coe, map_of_add_left_rel_zero, neg, nsmul, quot_mk_eq_coe, refl, rel_eq_coe, rel_mk, sInf_toSetoid, sSup_def, sSup_eq_addConGen, sub, sup_def, sup_eq_addConGen, toSetoid_bot, toSetoid_eq_bot, toSetoid_eq_top, toSetoid_inj, toSetoid_injective, toSetoid_top, trans, zsmul, coe_iInf, coe_inf, coe_inj, coe_mul, coe_one, coe_sInf, comap_rel, conGen_eq, conGen_idem, conGen_le, conGen_mono, conGen_of_con, div, eq, ext, ext', ext_iff, hrec_on₂_coe, induction_on, induction_on_units, induction_on₂, inf_iff_and, inv, le_def, liftOnUnits_mk, liftOn_coe, map_of_mul_left_rel_one, mul, mul', pow, quot_mk_eq_coe, refl, rel_eq_coe, rel_mk, sInf_toSetoid, sSup_def, sSup_eq_conGen, sup_def, sup_eq_conGen, toSetoid_bot, toSetoid_eq_bot, toSetoid_eq_top, toSetoid_inj, toSetoid_injective, toSetoid_top, trans, zpow | 94 |
| Total | 162 |
| Name | Category | Theorems |
|---|
addCommGroup 📖 | CompOp | — |
addCommMagma 📖 | CompOp | — |
addCommMonoid 📖 | CompOp | — |
addCommSemigroup 📖 | CompOp | — |
addGroup 📖 | CompOp | — |
addMonoid 📖 | CompOp | 1 mathmath: liftOnAddUnits_mk
|
addSemigroup 📖 | CompOp | — |
addZeroClass 📖 | CompOp | 18 mathmath: mk'_surjective, hom_ext_iff, lift_comp_mk', mrange_mk', comap_eq, coe_mk', kerLift_range_eq, kerLift_mk, mk'_ker, lift_mk', lift_range, kerLift_injective, lift_surjective_of_surjective, map_apply, lift_apply_mk', quotientKerEquivOfRightInverse_apply, lift_coe, coe_zero
|
comap 📖 | CompOp | 8 mathmath: comap_conGen_equiv, comapQuotientEquivOfSurj_symm_mk, comap_eq, comap_rel, comap_conGen_of_bijective, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, le_comap_conGen
|
gi 📖 | CompOp | — |
hasAdd 📖 | CompOp | 9 mathmath: ker_mkAddHom_eq, comapQuotientEquivOfSurj_symm_mk, coe_add, mkAddHom_apply, quotientKerEquivOfRightInverse_apply, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, congr_mk, quotientKerEquivOfRightInverse_symm_apply
|
hasNeg 📖 | CompOp | — |
hasSub 📖 | CompOp | — |
hrecOn₂ 📖 | CompOp | 1 mathmath: hrec_on₂_coe
|
instCoeTCQuotient 📖 | CompOp | — |
instCompleteLattice 📖 | CompOp | 10 mathmath: sSup_eq_addConGen, sup_def, toSetoid_top, toSetoid_bot, inf_iff_and, sSup_def, sup_eq_addConGen, toSetoid_eq_bot, toSetoid_eq_top, coe_inf
|
instDecidableEqQuotientOfDecidableCoeForallProp 📖 | CompOp | — |
instFunLikeForallProp 📖 | CompOp | 45 mathmath: sSup_eq_addConGen, eq, SymmetricPower.smul, sup_def, liftOnAddUnits_mk, add, coe_inj, coe_iInf, addConGen_idem, addConGen_of_addCon, AddLocalization.r_of_eq, ker_rel, inf_iff_and, quot_mk_eq_coe, rel_mk, le_def, mem_addSubgroup_iff, AddLocalization.r_iff_exists, vadd, finset_sum, multiset_sum, neg, AddLocalization.zero_rel, coe_sInf, ker_apply, AddSubmonoid.LocalizationMap.eq', map_of_add_left_rel_zero, AddLocalization.mk_eq_mk_iff, rel_eq_coe, sSup_def, nsmul, AddMonoid.Coprod.mk_eq_mk, comap_rel, sup_eq_addConGen, trans, symm, list_sum, ext_iff, map_apply, AddLocalization.r_iff_oreEqv_r, zsmul, sub, refl, coe_inf, AddMonoid.Coprod.con_neg_add_cancel
|
instInfSet 📖 | CompOp | 4 mathmath: coe_iInf, coe_sInf, addConGen_eq, sInf_toSetoid
|
instInhabited 📖 | CompOp | — |
instLE 📖 | CompOp | 11 mathmath: le_iff, le_def, AddSubgroup.orderIsoAddCon_symm_apply_coe, addConGen_mono, AddSubgroup.orderIsoAddCon_apply, orderIsoOp_apply, addConGen_le, QuotientAddGroup.con_mono, le_comap_conGen, orderIsoOp_symm_apply, QuotientAddGroup.con_le_iff
|
instMembershipProd 📖 | CompOp | 1 mathmath: mem_coe
|
instNSMulQuotientNat 📖 | CompOp | — |
instPartialOrder 📖 | CompOp | — |
instZSMul 📖 | CompOp | — |
liftOn 📖 | CompOp | 2 mathmath: liftOn_coe, CharacterModule.homEquiv_apply_apply
|
liftOnAddUnits 📖 | CompOp | 1 mathmath: liftOnAddUnits_mk
|
liftOn₂ 📖 | CompOp | — |
toQuotient 📖 | CompOp | 19 mathmath: eq, FreeAddMonoid.toPiTensorProduct, liftOnAddUnits_mk, quot_mk_eq_coe, comapQuotientEquivOfSurj_symm_mk, hrec_on₂_coe, coe_add, coe_mk', coe_vadd, kerLift_mk, mkAddHom_apply, liftOn_coe, map_apply, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, lift_coe, coe_zero, congr_mk, quotientKerEquivOfRightInverse_symm_apply
|
toSetoid 📖 | CompOp | 12 mathmath: toSetoid_top, toSetoid_bot, Module.DirectLimit.quotMk_of, ModuleCon.smul, rel_eq_coe, add', toSetoid_injective, toSetoid_eq_bot, comapQuotientEquivOfSurj_symm_mk', toSetoid_inj, sInf_toSetoid, toSetoid_eq_top
|
zero 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
comap 📖 | CompOp | 8 mathmath: comap_conGen_of_bijective, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, comapQuotientEquivOfSurj_symm_mk, comap_eq, le_comap_conGen, comap_conGen_equiv, comap_rel
|
commGroup 📖 | CompOp | — |
commMagma 📖 | CompOp | — |
commMonoid 📖 | CompOp | — |
commSemigroup 📖 | CompOp | — |
gi 📖 | CompOp | — |
group 📖 | CompOp | — |
hasDiv 📖 | CompOp | — |
hasInv 📖 | CompOp | — |
hasMul 📖 | CompOp | 9 mathmath: mkMulHom_apply, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, quotientKerEquivOfRightInverse_symm_apply, comapQuotientEquivOfSurj_symm_mk, quotientKerEquivOfRightInverse_apply, congr_mk, coe_mul, ker_mkMulHom_eq
|
hrecOn₂ 📖 | CompOp | 1 mathmath: hrec_on₂_coe
|
instCoeTCQuotient 📖 | CompOp | — |
instCompleteLattice 📖 | CompOp | 14 mathmath: RingCon.toCon_eq_bot, sup_eq_conGen, coe_inf, toSetoid_eq_bot, sSup_eq_conGen, sup_def, toSetoid_bot, inf_iff_and, sSup_def, RingCon.toCon_eq_top, toSetoid_top, toSetoid_eq_top, RingCon.toCon_bot, RingCon.toCon_top
|
instDecidableEqQuotientOfDecidableCoeForallProp 📖 | CompOp | — |
instFunLikeForallProp 📖 | CompOp | 49 mathmath: Localization.one_rel, mul, liftOnUnits_mk, RingCon.rel_mk, sup_eq_conGen, ker_rel, conGen_idem, div, inv, trans, refl, ker_apply, coe_inf, Monoid.Coprod.con_inv_mul_cancel, mem_subgroup_iff, rel_mk, PresentedMonoid.mk_eq_mk_iff, Localization.r_of_eq, Localization.r_iff_of_le_nonZeroDivisors, coe_iInf, eq, symm, rel_eq_coe, pow, sSup_eq_conGen, smul, coe_inj, sup_def, Localization.r_iff_exists, RingCon.coe_mk, conGen_of_con, le_def, Submonoid.LocalizationMap.eq', map_of_mul_left_rel_one, list_prod, inf_iff_and, coe_sInf, sSup_def, map_apply, Localization.r_iff_oreEqv_r, quot_mk_eq_coe, multiset_prod, finset_prod, RingCon.toCon_coe_eq_coe, Monoid.Coprod.mk_eq_mk, comap_rel, ext_iff, Localization.mk_eq_mk_iff, zpow
|
instInfSet 📖 | CompOp | 4 mathmath: sInf_toSetoid, conGen_eq, coe_iInf, coe_sInf
|
instInhabited 📖 | CompOp | — |
instLE 📖 | CompOp | 11 mathmath: le_iff, QuotientGroup.con_le_iff, orderIsoOp_symm_apply, conGen_le, Subgroup.orderIsoCon_apply, conGen_mono, orderIsoOp_apply, le_def, Subgroup.orderIsoCon_symm_apply_coe, QuotientGroup.con_mono, le_comap_conGen
|
instMembershipProd 📖 | CompOp | 1 mathmath: mem_coe
|
instPartialOrder 📖 | CompOp | — |
instPowQuotientNat 📖 | CompOp | — |
instZPow 📖 | CompOp | — |
liftOn 📖 | CompOp | 1 mathmath: liftOn_coe
|
liftOnUnits 📖 | CompOp | 1 mathmath: liftOnUnits_mk
|
liftOn₂ 📖 | CompOp | — |
monoid 📖 | CompOp | 1 mathmath: liftOnUnits_mk
|
mulOneClass 📖 | CompOp | 19 mathmath: hom_ext_iff, lift_surjective_of_surjective, mk'_surjective, kerLift_mk, lift_comp_mk', Monoid.CoprodI.of_apply, kerLift_range_eq, quotientKerEquivOfRightInverse_apply, comap_eq, coe_mk', coe_one, lift_mk', lift_coe, lift_apply_mk', mk'_ker, lift_range, map_apply, kerLift_injective, mrange_mk'
|
one 📖 | CompOp | — |
semigroup 📖 | CompOp | — |
toQuotient 📖 | CompOp | 18 mathmath: liftOnUnits_mk, mkMulHom_apply, kerLift_mk, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, liftOn_coe, eq, quotientKerEquivOfRightInverse_symm_apply, comapQuotientEquivOfSurj_symm_mk, coe_smul, coe_mk', hrec_on₂_coe, coe_one, congr_mk, lift_coe, coe_mul, map_apply, quot_mk_eq_coe
|
toSetoid 📖 | CompOp | 21 mathmath: RingCon.add', TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, sInf_toSetoid, RingCon.comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_symm_mk', RingCon.sInf_toSetoid, RingCon.factorₐ_mk, toSetoid_eq_bot, rel_eq_coe, RingCon.quotientQuotientEquivQuotientₐ_mk_mk, toSetoid_inj, RingCon.quotientQuotientEquivQuotient_mk_mk, toSetoid_bot, RingCon.quotientQuotientEquivQuotientₐ_symm_mk, TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r, toSetoid_injective, mul', toSetoid_top, RingCon.rel_eq_coe, RingCon.quotientQuotientEquivQuotient_symm_mk, toSetoid_eq_top
|
| Name | Category | Theorems |
|---|
AddCon 📖 | CompData | 63 mathmath: AddCon.sSup_eq_addConGen, AddCon.eq, SymmetricPower.smul, AddCon.sup_def, AddCon.toSetoid_top, AddCon.liftOnAddUnits_mk, AddCon.add, AddCon.coe_inj, AddCon.toSetoid_bot, AddCon.coe_iInf, AddCon.addConGen_idem, AddCon.addConGen_of_addCon, AddCon.le_iff, AddLocalization.r_of_eq, AddCon.ker_rel, AddCon.inf_iff_and, AddCon.quot_mk_eq_coe, AddCon.rel_mk, AddCon.le_def, AddCon.mem_addSubgroup_iff, AddLocalization.r_iff_exists, AddCon.vadd, AddCon.finset_sum, AddCon.multiset_sum, AddSubgroup.orderIsoAddCon_symm_apply_coe, AddCon.neg, AddLocalization.zero_rel, AddCon.coe_sInf, AddCon.ker_apply, AddSubmonoid.LocalizationMap.eq', AddCon.map_of_add_left_rel_zero, AddLocalization.mk_eq_mk_iff, AddCon.rel_eq_coe, AddCon.sSup_def, AddCon.nsmul, AddMonoid.Coprod.mk_eq_mk, AddCon.comap_rel, AddCon.sup_eq_addConGen, AddCon.trans, AddCon.symm, AddCon.list_sum, AddCon.addConGen_mono, AddCon.addConGen_eq, AddSubgroup.orderIsoAddCon_apply, AddCon.orderIsoOp_apply, AddCon.toSetoid_injective, AddCon.ext_iff, AddCon.map_apply, AddCon.addConGen_le, AddLocalization.r_iff_oreEqv_r, AddCon.toSetoid_eq_bot, QuotientAddGroup.con_mono, AddCon.zsmul, AddCon.le_comap_conGen, AddCon.sub, AddCon.orderIsoOp_symm_apply, QuotientAddGroup.con_le_iff, AddCon.sInf_toSetoid, AddCon.toSetoid_eq_top, AddCon.mem_coe, AddCon.refl, AddCon.coe_inf, AddMonoid.Coprod.con_neg_add_cancel
|
Con 📖 | CompData | 72 mathmath: Localization.one_rel, RingCon.toCon_eq_bot, Con.mul, Con.liftOnUnits_mk, RingCon.rel_mk, Con.le_iff, Con.sup_eq_conGen, RingCon.toCon_injective, Con.ker_rel, Con.conGen_idem, Con.div, Con.inv, Con.trans, Con.refl, Con.sInf_toSetoid, Con.ker_apply, QuotientGroup.con_le_iff, Con.coe_inf, Monoid.Coprod.con_inv_mul_cancel, Con.mem_subgroup_iff, Con.rel_mk, Con.mem_coe, Con.conGen_eq, Con.orderIsoOp_symm_apply, PresentedMonoid.mk_eq_mk_iff, Localization.r_of_eq, Con.conGen_le, Localization.r_iff_of_le_nonZeroDivisors, Con.toSetoid_eq_bot, Subgroup.orderIsoCon_apply, Con.coe_iInf, Con.eq, Con.symm, Con.rel_eq_coe, Con.pow, Con.sSup_eq_conGen, Con.smul, Con.coe_inj, Con.sup_def, Localization.r_iff_exists, Con.conGen_mono, Con.toSetoid_bot, RingCon.coe_mk, Con.orderIsoOp_apply, Con.conGen_of_con, Con.le_def, Submonoid.LocalizationMap.eq', Con.map_of_mul_left_rel_one, Con.toSetoid_injective, Con.list_prod, Subgroup.orderIsoCon_symm_apply_coe, QuotientGroup.con_mono, Con.le_comap_conGen, Con.inf_iff_and, Con.coe_sInf, Con.sSup_def, RingCon.toCon_eq_top, Con.map_apply, Con.toSetoid_top, Localization.r_iff_oreEqv_r, Con.toSetoid_eq_top, Con.quot_mk_eq_coe, Con.multiset_prod, Con.finset_prod, RingCon.toCon_coe_eq_coe, Monoid.Coprod.mk_eq_mk, Con.comap_rel, RingCon.toCon_bot, RingCon.toCon_top, Con.ext_iff, Localization.mk_eq_mk_iff, Con.zpow
|
addConGen 📖 | CompOp | 15 mathmath: AddCon.sSup_eq_addConGen, FreeAddMonoid.toPiTensorProduct, SymmetricPower.smul, AddCon.sup_def, AddCon.addConGen_idem, AddCon.addConGen_of_addCon, AddCon.comap_conGen_equiv, AddCon.sSup_def, AddCon.sup_eq_addConGen, AddCon.addConGen_mono, AddCon.addConGen_eq, AddCon.addConGen_le, AddCon.comap_conGen_of_bijective, AddCon.le_comap_conGen, CharacterModule.homEquiv_apply_apply
|
conGen 📖 | CompOp | 14 mathmath: Con.sup_eq_conGen, Con.conGen_idem, Con.comap_conGen_of_bijective, Con.conGen_eq, PresentedMonoid.mk_eq_mk_iff, Con.conGen_le, Monoid.CoprodI.of_apply, Con.sSup_eq_conGen, Con.sup_def, Con.conGen_mono, Con.conGen_of_con, Con.le_comap_conGen, Con.sSup_def, Con.comap_conGen_equiv
|