Commit 2025-12-11 08:08 36df19ca

View on Github →

feat(CategoryTheory/Localization): inverse in SmallShiftedHom (#32442) The post/precomposition on the types SmallShiftedHom W with a morphism which satisfies W is a bijection.

Estimated changes

Modified Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

added theorem CategoryTheory.Localization.SmallShiftedHom.comp_mk₀_id

added theorem CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv

added theorem CategoryTheory.Localization.SmallShiftedHom.mk₀Inv_comp_mk₀

added theorem CategoryTheory.Localization.SmallShiftedHom.mk₀_comp_mk₀Inv

added theorem CategoryTheory.Localization.SmallShiftedHom.mk₀_id_comp