Commit 2021-07-19 14:20 ad7ab8d8
View on Github →feat(linear_algebra/finsupp): span.repr gives an arbitrarily representation of x : span R w as a linear combination over w (#8339)
It's convenient to be able to get hold of such a representation, even when it is not unique. We prove the only lemma about this, then mark the definition is irreducible.