Theorems · Theorem · category theory
CategoryTheory.SingleObj.inv_as_inv
∀ (G : Type u) [inst : Group G] {x y : CategoryTheory.SingleObj G} (f : x ⟶ y), CategoryTheory.inv f = f⁻¹- Defined in
- Mathlib.CategoryTheory.SingleObj
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 15 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.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- Groupstatement and proof · cited by 6,238
- CategoryTheory.CategoryStruct.idproof · cited by 6,235
- CategoryTheory.invstatement · cited by 467
- inv_mul_cancelproof · cited by 107
- CategoryTheory.SingleObjstatement and proof · cited by 88
- CategoryTheory.IsIso.inv_eq_of_hom_inv_idproof · cited by 24
- CategoryTheory.SingleObj.id_as_oneproof · cited by 3
- CategoryTheory.SingleObj.comp_as_mulproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- Action.rightDual_ρproof · cited by 0
- IsFreeGroupoid.SpanningTree.endIsFreeproof · cited by 0
- Action.leftDual_ρproof · cited by 0