mathlib3
chore(data/prod): rename `injective_prod` to `injective.prod`
#2058
Merged
Merged
Commits
-
urkud committed 6 years ago
-
mergify[bot] committed 6 years ago
