mathlib
cc67cd75
- chore(*/centralizer): add forgotten `to_additive`s (#19168)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(*/centralizer): add forgotten `to_additive`s (#19168) I forgot these in #18861. These are already in the forward-port PR, leanprover-community/mathlib4#4896.
Author
ericrbg
Parents
59150e4a
Loading