mathlib3
b1f44ba1
- chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum (#1604)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum (#1604) * chore(order/zorn): rename zorn.zorn * chore(group_theory/free_group): rename sum.sum * chore(group_theory/free_group,order/zorn): remove nolint
References
#1604 - chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum
Author
robertylewis
Committer
mergify[bot]
Parents
5da754c9
Loading