mathlib3
d88ecd5b - chore(linear_algebra/std_basis): minor golfs (#14552)

Commit

3 years ago

chore(linear_algebra/std_basis): minor golfs (#14552)

Author

eric-wieser

eric-wieser

Parents

Loading