Quot

Statistics

Metric	Count
Definitions `Quot`, `factor`, `hrecOn₂`, `instDecidableLiftOnOfDecidablePred_mathlib`, `instDecidableLiftOn₂OfDecidablePred`, `instInhabited_mathlib`, `instUnique`, `decidablePred`, `liftOn₂`, `lift₂`, `decidablePred`, `map`, `mapRight`, `map₂`, `out`, `recOnSubsingleton₂`, `unquot`, `choice`, `eval`, `hrecOn'`, `hrecOn₂`, `hrecOn₂'`, `instDecidableLiftOn'OfDecidablePred`, `instDecidableLiftOnOfDecidablePred_mathlib`, `instDecidableLiftOn₂'OfDecidablePred`, `instDecidableLiftOn₂OfDecidablePred_mathlib`, `instInhabitedQuotient`, `instUniqueQuotient`, `decidablePred`, `liftOn'`, `liftOn₂'`, `decidablePred`, `map`, `map'`, `map₂`, `map₂'`, `mk''`, `out`, `recOnSubsingleton'`, `recOnSubsingleton₂'`, `«term⟦_⟧»`, `instCoeFunForallForallProp_mathlib`, `bind`, `instInhabited`, `instMonad`, `liftOn`, `map`, `mk`, `out`, `rec`, `recOn`, `recOnSubsingleton`, `piSetoid`, `trueSetoid`	54
Theorems `quot_mk_eq_iff`, `eq`, `factor_mk_eq`, `induction_on`, `induction_on₂`, `induction_on₃`, `liftOn_mk`, `liftOn₂_mk`, `lift_mk`, `lift₂_mk`, `map₂_mk`, `mk_surjective`, `out_eq`, `surjective_lift`, `choice_eq`, `eq`, `eq'`, `eq''`, `eq_iff_equiv`, `eq_mk_iff_out`, `eval_mk`, `exact'`, `exists`, `forall`, `hrecOn'_mk''`, `hrecOn₂'_mk''`, `ind'`, `inductionOn'`, `inductionOn₂'`, `inductionOn₃'`, `induction_on_pi`, `ind₂'`, `instIsEquivEquiv`, `instSubsingletonQuotient`, `liftOn'_mk`, `liftOn'_mk''`, `liftOn_mk`, `liftOn₂'_mk`, `liftOn₂'_mk''`, `liftOn₂_mk`, `lift_comp_mk`, `lift_mk`, `lift_surjective`, `lift_surjective_iff`, `lift₂_mk`, `map'_mk`, `map'_mk''`, `map_mk`, `map₂'_mk''`, `map₂_mk`, `mk''_eq_mk`, `mk''_surjective`, `mk'_surjective`, `mk_eq_iff_out`, `mk_out`, `mk_out'`, `mk_surjective`, `out_eq`, `out_eq'`, `out_equiv_out`, `out_inj`, `out_injective`, `sound'`, `surjective_liftOn'`, `ext`, `eq`, `exists_rep`, `ind`, `induction_on`, `induction_on₂`, `instLawfulMonad`, `instSubsingletonTrunc`, `lift_mk`, `nonempty`, `out_eq`, `nonempty_quotient_iff`, `true_equivalence`	77
Total	131

AddCommGrpCat.Colimits

Definitions

Name	Category	Theorems
`Quot` 📖	CompOp	14 math math: `AddCommGrpCat.isColimit_iff_bijective_desc`, `AddCommGrpCat.instSmallQuot`, `colimitCocone_ι_app`, `quotUliftToQuot_ι`, `colimitCocone_pt`, `Quot.desc_toCocone_desc`, `quotToQuotUlift_ι`, `Quot.desc_colimitCocone`, `Quot.desc_toCocone_desc_app`, `toCocone_ι_app`, `Quot.ι_desc`, `Quot.map_ι`, `Quot.desc_quotQuotUliftAddEquiv`, `AddCommGrpCat.hasColimit_iff_small_quot`

Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quot_mk_eq_iff` 📖	—	—	—	—	`Quotient.eq`

Quot

Definitions

Name	Category	Theorems
`factor` 📖	CompOp	1 math math: `factor_mk_eq`
`hrecOn₂` 📖	CompOp	—
`instDecidableLiftOnOfDecidablePred_mathlib` 📖	CompOp	—
`instDecidableLiftOn₂OfDecidablePred` 📖	CompOp	—
`instInhabited_mathlib` 📖	CompOp	—
`instUnique` 📖	CompOp	—
`liftOn₂` 📖	CompOp	1 math math: `liftOn₂_mk`
`lift₂` 📖	CompOp	1 math math: `lift₂_mk`
`map` 📖	CompOp	2 math math: `FreeAddGroup.quot_map_mk`, `FreeGroup.quot_map_mk`
`mapRight` 📖	CompOp	—
`map₂` 📖	CompOp	1 math math: `map₂_mk`
`out` 📖	CompOp	9 math math: `HomotopyCategory.quotient_map_out_comp_out`, `out_eq`, `Sym2.out_fst_mem`, `SimpleGraph.ConnectedComponent.Represents.image_out`, `Associates.mk_quot_out`, `HomotopyCategory.quotient_map_out`, `Associates.quot_out_zero`, `Sym2.out_snd_mem`, `Associates.quot_out`
`recOnSubsingleton₂` 📖	CompOp	—
`unquot` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`Relation.EqvGen`	—	`eqvGen_exact` `eqvGen_sound`
`factor_mk_eq` 📖	mathematical	—	`factor`	—	—
`induction_on` 📖	—	—	—	—	—
`induction_on₂` 📖	—	—	—	—	—
`induction_on₃` 📖	—	—	—	—	—
`liftOn_mk` 📖	—	—	—	—	—
`liftOn₂_mk` 📖	mathematical	—	`liftOn₂`	—	—
`lift_mk` 📖	—	—	—	—	—
`lift₂_mk` 📖	mathematical	—	`lift₂`	—	—
`map₂_mk` 📖	mathematical	—	`map₂`	—	—
`mk_surjective` 📖	—	—	—	—	—
`out_eq` 📖	mathematical	—	`out`	—	—
`surjective_lift` 📖	—	—	—	—	—

Quot.lift

Definitions

Name	Category	Theorems
`decidablePred` 📖	CompOp	—

Quot.lift₂

Definitions

Name	Category	Theorems
`decidablePred` 📖	CompOp	—

Quotient

Definitions

Name	Category	Theorems
`choice` 📖	CompOp	1 math math: `choice_eq`
`eval` 📖	CompOp	3 math math: `eval_finChoice`, `eval_mk`, `finChoiceEquiv_symm_apply`
`hrecOn'` 📖	CompOp	2 math math: `hrecOn'_mk''`, `hrecOn₂'_mk''`
`hrecOn₂` 📖	CompOp	—
`hrecOn₂'` 📖	CompOp	1 math math: `hrecOn₂'_mk''`
`instDecidableLiftOn'OfDecidablePred` 📖	CompOp	—
`instDecidableLiftOnOfDecidablePred_mathlib` 📖	CompOp	—
`instDecidableLiftOn₂'OfDecidablePred` 📖	CompOp	—
`instDecidableLiftOn₂OfDecidablePred_mathlib` 📖	CompOp	—
`instInhabitedQuotient` 📖	CompOp	—
`instUniqueQuotient` 📖	CompOp	—
`liftOn'` 📖	CompOp	10 math math: `liftOn'_mk`, `liftOn'_mk''`, `Topology.IsQuotientMap.lift_apply`, `QuotientAddGroup.quotient_liftOn_mk`, `QuotientGroup.quotient_liftOn_mk`, `surjective_liftOn'`, `Setoid.prodQuotientEquiv_symm_apply`, `Setoid.piQuotientEquiv_symm_apply`, `Set.range_quotient_lift_on'`, `Continuous.quotient_liftOn'`
`liftOn₂'` 📖	CompOp	5 math math: `liftOn₂'_mk`, `WellFounded.quotient_liftOn₂'`, `acc_liftOn₂'_iff`, `liftOn₂'_mk''`, `wellFounded_liftOn₂'_iff`
`map` 📖	CompOp	3 math math: `CategoryTheory.ThinSkeleton.map_map`, `CategoryTheory.ThinSkeleton.map_obj`, `map_mk`
`map'` 📖	CompOp	15 math math: `AddSubgroup.quotientEquivProdOfLE_symm_apply`, `OrderHom.antisymmetrization_apply`, `Subgroup.quotientEquivProdOfLE_apply`, `OrderHom.coe_antisymmetrization`, `map₂'_mk''`, `Subgroup.quotientEquivProdOfLE_symm_apply`, `map'_mk`, `Subgroup.quotientEquivProdOfLE'_symm_apply`, `Continuous.quotient_map'`, `AddSubgroup.quotientEquivProdOfLE'_apply`, `Subgroup.quotientEquivProdOfLE'_apply`, `AddSubgroup.quotientEquivProdOfLE'_symm_apply`, `AddSubgroup.quotientEquivProdOfLE_apply`, `map'_mk''`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul`
`map₂` 📖	CompOp	2 math math: `Setoid.prodQuotientEquiv_apply`, `map₂_mk`
`map₂'` 📖	CompOp	1 math math: `map₂'_mk''`
`mk''` 📖	CompOp	51 math math: `sound'`, `AlternatingMap.domCoprod.summand_mk''`, `out_eq'`, `AddSubgroup.IsComplement.quotientAddGroupMk_leftQuotientEquiv`, `AddCircle.equivIccQuot_comp_mk_eq_toIcoMod`, `liftOn'_mk''`, `Subgroup.quotientEquivProdOfLE_apply`, `Topology.IsQuotientMap.homeomorph_symm_apply`, `eq''`, `AddSubgroup.isComplement_addSubgroup_left_iff_bijective`, `AddSubgroup.IsComplement.mk''_rightQuotientEquiv`, `Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk''`, `NumberField.InfinitePlace.orbitRelEquiv_apply_mk''`, `map₂'_mk''`, `CategoryTheory.Subobject.inf_eq_map_pullback'`, `AddCircle.equivIccQuot_comp_mk_eq_toIocMod`, `HomogeneousLocalization.zero_eq`, `Set.Quotient.range_mk''`, `AddAction.orbitRel.Quotient.mem_orbit`, `Setoid.prodQuotientEquiv_symm_apply`, `Setoid.ker_mk_eq`, `AddSubgroup.isComplement_addSubgroup_left_iff_existsUnique_quotientMk''`, `mk''_surjective`, `Cycle.mk''_eq_coe`, `MulAction.orbitRel.Quotient.orbit_mk`, `HomogeneousLocalization.one_eq`, `Function.RightInverse.homeomorph_symm_apply`, `Setoid.piQuotientEquiv_symm_apply`, `measurable_from_quotient`, `Subgroup.isComplement_subgroup_left_iff_bijective`, `AddSubgroup.quotientEquivProdOfLE'_apply`, `Path.Homotopic.Quotient.mk''_eq_mk`, `Subgroup.IsComplement.mk''_rightQuotientEquiv`, `mk_out'`, `Subgroup.quotientEquivProdOfLE'_apply`, `Setoid.piQuotientEquiv_apply`, `MulAction.orbitRel.Quotient.mem_orbit`, `AddSubgroup.quotientEquivProdOfLE_apply`, `CategoryTheory.Subobject.inf_eq_map_pullback`, `Setoid.quotientKerEquivOfRightInverse_symm_apply`, `map'_mk''`, `acc_liftOn₂'_iff`, `liftOn₂'_mk''`, `measurableSet_quotient`, `Submodule.Quotient.mk''_eq_mk`, `Setoid.comap_eq`, `AddAction.orbitRel.Quotient.orbit_mk`, `mk''_eq_mk`, `measurable_quotient_mk''`, `Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv`, `LieSubmodule.Quotient.is_quotient_mk`
`out` 📖	CompOp	69 math math: `MulAction.Quotient.coe_smul_out`, `Setoid.ker_apply_mk_out`, `AddSubgroup.quotientEquivProdOfLE_symm_apply`, `out_eq'`, `mk_eq_iff_out`, `QuotientAddGroup.univ_eq_iUnion_vadd`, `MulAction.quotient_out_smul_fixedPoints`, `CommRing.Pic.mul_eq_tensor`, `QuotientGroup.out_eq'`, `Subgroup.quotientEquivProdOfLE_apply`, `Cardinal.mk_out`, `CategoryTheory.ThinSkeleton.fromThinSkeleton_map`, `AddAction.Quotient.coe_vadd_out`, `ZFSet.mk_out`, `out_injective`, `CategoryTheory.ThinSkeleton.fromThinSkeleton_obj`, `CategoryTheory.skeletonEquivalence_unitIso`, `MulAction.card_eq_sum_card_group_div_card_stabilizer`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `out_equiv_out`, `CommRing.Pic.inv_eq_dual`, `outRelEmbedding_apply`, `CommRing.Pic.mk_eq_iff`, `QuotientGroup.univ_eq_iUnion_smul`, `CommRing.Pic.mk_eq_self`, `CommRing.Pic.mapAlgebra_apply`, `AddAction.Quotient.mk_vadd_out`, `CommRing.Pic.ext_iff`, `CommRing.Pic.instFreeAsModuleOfNat`, `Subgroup.quotientEquivProdOfLE_symm_apply`, `QuotientAddGroup.mk_out_eq_mul`, `QuotientGroup.mk_out_eq_mul`, `Subgroup.quotientEquivSigmaZMod_apply`, `CategoryTheory.fromSkeleton_obj`, `QuotientGroup.orbit_eq_out_smul`, `QuotientAddGroup.out_eq'`, `MulAction.Quotient.mk_smul_out`, `CategoryTheory.fromSkeleton_map`, `Function.Embedding.coe_quotientOut`, `Subgroup.transferTransversal_apply'`, `eq_mk_iff_out`, `Cardinal.nonempty_out`, `Ideal.Quotient.mk_out`, `CategoryTheory.Skeleton.comp_hom`, `QuotientAddGroup.orbit_eq_out_vadd`, `CategoryTheory.toSkeletonFunctor_map_hom`, `Submodule.Quotient.mk_out`, `Ideal.univ_eq_iUnion_image_add`, `Cardinal.out_lift_equiv`, `mk_out'`, `Subgroup.transferFunction_apply`, `Setoid.piQuotientEquiv_apply`, `DoubleCoset.disjoint_out`, `out_inj`, `Subgroup.transferTransversal_apply''`, `AddSubgroup.quotientEquivProdOfLE_apply`, `AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer`, `CategoryTheory.Skeleton.mul_eq`, `Subgroup.quotientEquivSigmaZMod_symm_apply`, `out_eq`, `DoubleCoset.out_eq'`, `instInvertibleCarrierOutModuleCatValSkeleton`, `mk_out`, `IndexedPartition.index_out`, `MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot`, `Cardinal.out_embedding`, `CategoryTheory.Skeleton.comp_hom_assoc`, `QuotientGroup.out_conj_pow_minimalPeriod_mem`, `DoubleCoset.mk_out_eq_mul`
`recOnSubsingleton'` 📖	CompOp	—
`recOnSubsingleton₂'` 📖	CompOp	—
`«term⟦_⟧»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`choice_eq` 📖	mathematical	—	`choice` `piSetoid`	—	`mk_out`
`eq` 📖	—	—	—	—	—
`eq'` 📖	—	—	—	—	`eq`
`eq''` 📖	mathematical	—	`mk''`	—	`eq`
`eq_iff_equiv` 📖	—	—	—	—	`eq`
`eq_mk_iff_out` 📖	mathematical	—	`out`	—	`out_eq` `eq`
`eval_mk` 📖	mathematical	—	`eval` `piSetoid`	—	—
`exact'` 📖	—	`mk''`	—	—	—
`exists` 📖	—	—	—	—	—
`forall` 📖	—	—	—	—	—
`hrecOn'_mk''` 📖	mathematical	`mk''`	`hrecOn'`	—	—
`hrecOn₂'_mk''` 📖	mathematical	`mk''`	`hrecOn₂'` `hrecOn'`	—	—
`ind'` 📖	—	`mk''`	—	—	—
`inductionOn'` 📖	—	`mk''`	—	—	—
`inductionOn₂'` 📖	—	`mk''`	—	—	—
`inductionOn₃'` 📖	—	`mk''`	—	—	—
`induction_on_pi` 📖	—	—	—	—	`out_eq`
`ind₂'` 📖	—	`mk''`	—	—	—
`instIsEquivEquiv` 📖	mathematical	—	`IsEquiv`	—	—
`instSubsingletonQuotient` 📖	—	—	—	—	`Quot.Subsingleton`
`liftOn'_mk` 📖	mathematical	—	`liftOn'`	—	—
`liftOn'_mk''` 📖	mathematical	—	`liftOn'` `mk''`	—	—
`liftOn_mk` 📖	—	—	—	—	—
`liftOn₂'_mk` 📖	mathematical	—	`liftOn₂'`	—	—
`liftOn₂'_mk''` 📖	mathematical	—	`liftOn₂'` `mk''`	—	—
`liftOn₂_mk` 📖	—	—	—	—	—
`lift_comp_mk` 📖	—	—	—	—	—
`lift_mk` 📖	—	—	—	—	—
`lift_surjective` 📖	—	—	—	—	`Quot.surjective_lift`
`lift_surjective_iff` 📖	—	—	—	—	`Quot.surjective_lift`
`lift₂_mk` 📖	—	—	—	—	—
`map'_mk` 📖	mathematical	—	`map'`	—	—
`map'_mk''` 📖	mathematical	—	`map'` `mk''`	—	—
`map_mk` 📖	mathematical	—	`map`	—	—
`map₂'_mk''` 📖	mathematical	—	`map₂'` `mk''` `map'`	—	—
`map₂_mk` 📖	mathematical	—	`map₂`	—	—
`mk''_eq_mk` 📖	mathematical	—	`mk''`	—	—
`mk''_surjective` 📖	mathematical	—	`mk''`	—	—
`mk'_surjective` 📖	—	—	—	—	—
`mk_eq_iff_out` 📖	mathematical	—	`out`	—	`out_eq` `eq`
`mk_out` 📖	mathematical	—	`out`	—	`out_eq`
`mk_out'` 📖	mathematical	—	`out` `mk''`	—	`out_eq`
`mk_surjective` 📖	—	—	—	—	—
`out_eq` 📖	mathematical	—	`out`	—	`Quot.out_eq`
`out_eq'` 📖	mathematical	—	`mk''` `out`	—	`out_eq`
`out_equiv_out` 📖	mathematical	—	`out`	—	`eq_mk_iff_out` `out_eq`
`out_inj` 📖	mathematical	—	`out`	—	`out_injective`
`out_injective` 📖	mathematical	—	`out`	—	`out_equiv_out`
`sound'` 📖	mathematical	—	`mk''`	—	—
`surjective_liftOn'` 📖	mathematical	—	`liftOn'`	—	`Quot.surjective_lift`

Quotient.lift

Definitions

Name	Category	Theorems
`decidablePred` 📖	CompOp	—

Quotient.lift₂

Definitions

Name	Category	Theorems
`decidablePred` 📖	CompOp	—

Setoid

Definitions

Name	Category	Theorems
`instCoeFunForallForallProp_mathlib` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	—

Trunc

Definitions

Name	Category	Theorems
`bind` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMonad` 📖	CompOp	1 math math: `instLawfulMonad`
`liftOn` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `MultilinearMap.dfinsuppFamily_apply_support'`, `DirectSum.addEquivProdDirectSum_symm_apply_support'`, `finChoiceEquiv_symm_apply`
`mk` 📖	CompOp	—
`out` 📖	CompOp	1 math math: `out_eq`
`rec` 📖	CompOp	—
`recOn` 📖	CompOp	—
`recOnSubsingleton` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	—	—	—	—	`induction_on₂`
`exists_rep` 📖	—	—	—	—	—
`ind` 📖	—	—	—	—	—
`induction_on` 📖	—	—	—	—	`ind`
`induction_on₂` 📖	—	—	—	—	`induction_on`
`instLawfulMonad` 📖	mathematical	—	`Trunc` `instMonad`	—	`eq`
`instSubsingletonTrunc` 📖	mathematical	—	`Trunc`	—	`eq`
`lift_mk` 📖	mathematical	—	`lift`	—	—
`nonempty` 📖	—	—	—	—	`exists_rep`
`out_eq` 📖	mathematical	—	`out`	—	`eq`

(root)

Definitions

Name	Category	Theorems
`piSetoid` 📖	CompOp	13 math math: `Quotient.listChoice_mk`, `QuotientAddGroup.rightRel_pi`, `Quotient.finChoiceEquiv_apply`, `Setoid.piSetoid_apply`, `Quotient.eval_mk`, `Setoid.piQuotientEquiv_symm_apply`, `Quotient.choice_eq`, `Quotient.finChoice_eq`, `Setoid.piQuotientEquiv_apply`, `QuotientGroup.rightRel_pi`, `Quotient.finChoiceEquiv_symm_apply`, `QuotientAddGroup.leftRel_pi`, `QuotientGroup.leftRel_pi`
`trueSetoid` 📖	CompOp	2 math math: `Trunc.finLiftOn_mk`, `Trunc.finRecOn_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_quotient_iff` 📖	—	—	—	—	—
`true_equivalence` 📖	—	—	—	—	—

---

← Back to Index