Theorems · Theorem · category theory
Action.diagonalSuccIsoTensorTrivial_inv_hom_apply
∀ {G : Type u} [inst : Group G] {n : ℕ} (g : G) (f : Fin n → G),
(CategoryTheory.ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f- Defined in
- Mathlib.CategoryTheory.Action.Monoidal
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites45
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Iso.homproof · cited by 7,684
- CategoryTheory.Iso.invstatement and proof · cited by 6,514
- CategoryTheory.Category.assocproof · cited by 6,433
- Groupstatement and proof · cited by 6,238
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- mul_oneproof · cited by 3,885
- Equiv.symmproof · cited by 3,681
- CategoryTheory.MonoidalCategoryStruct.tensorObjstatement and proof · cited by 3,106
- mul_assocproof · cited by 1,667
- TypeCat.Funstatement · cited by 1,307
Cited by1
Results whose statement or proof uses this declaration.
- Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eqproof · cited by 0