Theorems · Definition · category theory
Action.ofMulAction
(G : Type u_1) → (H : Type u) → [inst : Monoid G] → [MulAction G H] → Action (Type u) G
Bundles a type H with a multiplicative action of G as an Action.
- Defined in
- Mathlib.CategoryTheory.Action.Concrete
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- MulActionstatement and proof · cited by 1,294
- MonoidHom.compproof · cited by 469
- Actionstatement · cited by 206
- MulEquiv.toMonoidHomproof · cited by 126
- TypeCat.endEquivproof · cited by 3
- MulAction.toEndHomproof · cited by 1
Cited by15
Results whose statement or proof uses this declaration.
- Action.leftRegularproof · cited by 8
- Action.diagonalproof · cited by 5
- classifyingSpaceUniversalCoverproof · cited by 4
- Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eqproof · cited by 2
- Rep.standardComplex.d_eqproof · cited by 1
- Rep.linearizationOfMulActionIsostatement · cited by 1
- classifyingSpaceUniversalCover_mapstatement · cited by 0
- Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eqproof · cited by 0
- classifyingSpaceUniversalCover.cechNerveTerminalFromIsostatement · cited by 0
- Representation.linearizeOfMulActionIsostatement and proof · cited by 0
- Action.ofMulActionLimitConestatement and proof · cited by 0
- Action.ofMulAction_Vstatement and proof · cited by 0