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
