Mathlib Changelog
v4
Changelog
About
Github
Def
CategoryTheory.NormalMono.ofArrowIso
Modification history
2026-01-29 18:03
Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean
feat(CategoryTheory): transport a NormalMono structure via an isomorphism of arrows (#34496)
Added
CategoryTheory.NormalMono.ofArrowIso
View on Github →