mathlib3
2a8d7f3e - chore(analysis/normed_space/banach): correct typo (#3840)

Commit
5 years ago
chore(analysis/normed_space/banach): correct typo (#3840) Correct a typo from an old global replace.
Author
Parents
Loading