Documentation Verification Report

HomCongr

📁 Source: Mathlib/CategoryTheory/Enriched/HomCongr.lean

Statistics

Metric	Count
Definitions `eHomCongr`	1
Theorems `eHomCongr_comp`, `eHomCongr_comp_assoc`, `eHomCongr_hom`, `eHomCongr_inv`, `eHomCongr_inv_comp`, `eHomCongr_inv_comp_assoc`, `eHomCongr_refl`, `eHomCongr_symm`, `eHomCongr_trans`	9
Total	10

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`eHomCongr` 📖	CompOp	9 math math: `eHomCongr_refl`, `eHomCongr_inv_comp_assoc`, `eHomCongr_hom`, `eHomCongr_symm`, `eHomCongr_comp_assoc`, `eHomCongr_trans`, `eHomCongr_comp`, `eHomCongr_inv`, `eHomCongr_inv_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eHomCongr_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.eHomEquiv` `hom` `eHomCongr` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.eComp`	—	`CategoryTheory.MonoidalCategory.whiskerRight_id` `CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc` `hom_inv_id_assoc` `CategoryTheory.MonoidalCategory.whisker_exchange_assoc` `CategoryTheory.eComp_eHomWhiskerLeft` `CategoryTheory.eHom_whisker_cancel_assoc` `CategoryTheory.eComp_eHomWhiskerRight_assoc` `CategoryTheory.MonoidalCategory.tensorHom_def_assoc` `CategoryTheory.eHomEquiv_comp_assoc`
`eHomCongr_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.eHomEquiv` `hom` `eHomCongr` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.eComp`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `eHomCongr_comp`
`eHomCongr_hom` 📖	mathematical	—	`hom` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `eHomCongr` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eHomWhiskerRight` `inv` `CategoryTheory.eHomWhiskerLeft`	—	—
`eHomCongr_inv` 📖	mathematical	—	`inv` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `eHomCongr` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eHomWhiskerRight` `hom` `CategoryTheory.eHomWhiskerLeft`	—	—
`eHomCongr_inv_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.eHomEquiv` `inv` `eHomCongr` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.eComp`	—	`eHomCongr_comp`
`eHomCongr_inv_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.eHomEquiv` `inv` `eHomCongr` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.eComp`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `eHomCongr_inv_comp`
`eHomCongr_refl` 📖	mathematical	—	`eHomCongr` `refl` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory`	—	`ext` `CategoryTheory.eHomWhiskerRight_id` `CategoryTheory.eHomWhiskerLeft_id` `CategoryTheory.Category.comp_id`
`eHomCongr_symm` 📖	mathematical	—	`symm` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `eHomCongr`	—	—
`eHomCongr_trans` 📖	mathematical	—	`eHomCongr` `trans` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory`	—	`ext` `CategoryTheory.eHomWhiskerRight_comp` `CategoryTheory.eHomWhiskerLeft_comp` `CategoryTheory.Category.assoc` `CategoryTheory.eHom_whisker_exchange_assoc`

---

← Back to Index