mathlib
3a2039ad
- chore(linear_algebra/dimension): remove outdated comment (#18759)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(linear_algebra/dimension): remove outdated comment (#18759) This used to be about `vector_space.dim`, but was caught up in the rename that fixed the naming inconsistency and is now nonsense.
Author
eric-wieser
Parents
f29120f8
Loading