Documentation Verification Report

CommSq

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Statistics

MetricCount
DefinitionsCommSq
1
Theorems0
Total1

CategoryTheory

Definitions

NameCategoryTheorems
CommSq 📖CompData
21 mathmath: Lattice.BicartSq.commSq, IsHomLift.commSq, CommSq.vert_inv, CommSq.toLoc, CommSq.horiz_inv, Functor.map_commSq, CommSq.flip, AlgebraicGeometry.ValuativeCommSq.commSq, HasLiftingProperty.transfiniteComposition.SqStruct.sq, Square.commSq, CommSq.right_adjoint, CommSq.unop, CommSq.of_arrow, CommSq.op, CommSq.left_adjoint, IsPushout.toCommSq, MonoOver.commSqOfHasStrongEpiMonoFactorisation, CommSq.map, IsPullback.toCommSq, CommSq.vert_comp, CommSq.horiz_comp

---

← Back to Index