Def CategoryTheory.normalOfIsPushoutFstOfNormal

Modification history

2023-03-08 20:49

Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

feat: port CategoryTheory.Limits.Shapes.NormalMono.Basic (#2732)

Added CategoryTheory.normalOfIsPushoutFstOfNormal View on Github →