mathlib3
862854ed
- chore(ring_theory/localization): fix typo in module docstring (#11245)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(ring_theory/localization): fix typo in module docstring (#11245) There was a mismatch in the module docstring to the decl name later.
Author
pechersky
Parents
dc352a64
Loading