Theorem CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso_inv_left

Modification history

2026-10-20 15:02
Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean
feat(CategoryTheory): kan extensions from isos (#41484) …
Added CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso_inv_leftView on Github →