mathlib
11c53f17 - fix(*): use `old_structure_cmd` for all morphism classes (#16242)

Commit
3 years ago
fix(*): use `old_structure_cmd` for all morphism classes (#16242) This PR changes all morphism classes to use the old structure command, as briefly discussed [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/old_structure_cmd.20in.20morphism.20type.20classes). Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Author
Parents
Loading