chore(linear_algebra/alternating): golf using injective APIs (#12536)
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.





leanprover-community/mathlib,leanprover-community/mathlib