mathlib
937c692d - chore(category_theory): fix name of mono_app_of_mono (#16275)

Commit

3 years ago

chore(category_theory): fix name of mono_app_of_mono (#16275) This PR fixes the names of a few lemmas like `mono_app_of_mono`.

Author

joelriou

Parents