mathlib3

87c54600 - refactor(linear_algebra/bilinear_map): move lemmas about `basis` to a new file. (#18468)

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.