chore(linear_algebra/bilinear_form): cleanup (#5049)

- Generalize some defs and lemmas to semimodules over semirings
- Define the equiv between `bilin_form` and `linear_map` analogously to `linear_map.to_matrix / matrix.to_lin`
- Mark appropriate lemmas as `simp`
- Fix overlong lines, match style guide in other places too
- Make use of variables consistent throughout the file

Author: Vierkantor

scripts/copy-mod-doc-exceptions.txt

@@ -1156,13 +1156,6 @@ src/linear_algebra/basic.lean : line 2054 : ERR_LIN : Line has more than 100 cha
 src/linear_algebra/basic.lean : line 2112 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/basic.lean : line 2180 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 106 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 154 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 368 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 621 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 623 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 658 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/bilinear_form.lean : line 98 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/char_poly/coeff.lean : line 190 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/char_poly/coeff.lean : line 24 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/char_poly/coeff.lean : line 26 : ERR_LIN : Line has more than 100 characters