mathlib
d50b12ae - fix(*): fix typo in the word subtraction (#18145)

Commit

3 years ago

fix(*): fix typo in the word subtraction (#18145) Wiktionary defines "substraction" as "(obsolete or non-native speakers' English) Subtraction."

Author

eric-wieser

Parents