mathlib3
5d405e2a - chore(linear_algebra/alternating): golf using injective APIs (#12536)

Commit

3 years ago

chore(linear_algebra/alternating): golf using injective APIs (#12536) To do this, we have to move the has_scalar instance higher up in the file.

Author

eric-wieser

Parents