Theorems · Definition · group theory
Shrink.mulEquiv
{α : Type u_2} → [inst : Small.{v, u_2} α] → [inst_1 : Mul α] → Shrink.{v, u_2} α ≃* αShrink α to a smaller universe preserves multiplication.
- Defined in
- Mathlib.Algebra.Group.Shrink
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.symmproof · cited by 3,681
- MulEquivstatement · cited by 1,142
- Smallstatement and proof · cited by 369
- Shrinkstatement · cited by 132
- equivShrinkproof · cited by 118
- Equiv.mulEquivproof · cited by 3
Cited by14
Results whose statement or proof uses this declaration.
- GrpCat.shrinkFunctorproof · cited by 6
- MonCat.shrinkFunctorproof · cited by 6
- CategoryTheory.shrinkYonedaGrpObjObjEquivproof · cited by 3
- CategoryTheory.shrinkYonedaMonObjObjEquivproof · cited by 3
- GrpCat.shrinkFunctorMapproof · cited by 2
- MonCat.shrinkFunctorMapproof · cited by 2
- CategoryTheory.shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symmproof · cited by 1
- CategoryTheory.shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symmproof · cited by 1
- MonCat.shrinkFunctor_mapstatement · cited by 0
- GrpCat.shrinkFunctorMap_appstatement · cited by 0
- GrpCat.shrinkFunctor_mapstatement · cited by 0
- CategoryTheory.shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symmproof · cited by 0