mathlib3
aa669096 - chore(algebraic_geometry): Remove unwanted spaces. (#11042)

Commit

4 years ago

chore(algebraic_geometry): Remove unwanted spaces. (#11042) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author

erdOne

Parents