mathlib
6b9d5860 - chore(linear_algebra): use `to_span_singleton` instead of `id.smul_right`

Commit

3 years ago

chore(linear_algebra): use `to_span_singleton` instead of `id.smul_right` Since we have this definition, we may as well use it.

References

Author

eric-wieser

Parents