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.ofArrowIsoView on Github →