mathlib3
chore(data/prod): rename `injective_prod` to `injective.prod`
#2058
Merged
Merged
chore(data/prod): rename `injective_prod` to `injective.prod` #2058
mergify
merged
2 commits into
master
from
injective-prod
chore(data/prod): rename `injective_prod` to `injective.prod`
76a3da81
jcommelin
approved these changes
on 2020-02-26
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into injective-prod
2b5f0f81
Login to write a write a comment.
Login via GitHub