mathlib3
5129aed5
- chore(algebra/group/to_additive): improve warning message (#3024)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra/group/to_additive): improve warning message (#3024) Also prevent `group_theory/subgroup` from generating this warning.
Author
urkud
Parents
ade196f8
Loading