Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911)

Commit

2 years ago

chore(category_theory/monoidal/Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911) This matches the existing `Mon_`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

362c2263

mathlib 33085c97 - chore(category_theory/monoidal/Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911)

mathlib
33085c97 - chore(category_theory/monoidal/Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911)