Commit 2023-02-21 21:07 87c54600

refactor(linear_algebra/bilinear_map): move lemmas about basis to a new file. (#18468) This cuts the import path. The copyright comes from #12269. I chose not to just move these lemmas to linear_algebra/basis as this file is already huge. The moved lemmas are now stated slightly more generally (comm_semiring rather than comm_ring), which seems to have been an accident in the original file as no proofs had to change.