mathlib3

d0789503 - feat(linear_algebra/bilinear_form): equivalence with matrices, given a basis (#5095)

feat(linear_algebra/bilinear_form): equivalence with matrices, given a basis (#5095) This PR defines the equivalence between bilinear forms on an arbitrary module and matrices, given a basis of that module. It updates the existing equivalence between bilinear forms on `n → R` so that the overall structure of the file matches that of `linear_algebra.matrix`, i.e. there are two pairs of equivs, one for `n → R` and one for any `M` with a basis. Changes: - `bilin_form_equiv_matrix`, `bilin_form.to_matrix` and `matrix.to_bilin_form` have been consolidated as linear equivs `bilin_form.to_matrix'` and `matrix.to_bilin'`. Other declarations have been renamed accordingly. - `quadratic_form.to_matrix` and `matrix.to_quadratic_form` are renamed by analogy to `quadratic_form.to_matrix'` and `matrix.to_quadratic_form'` - replaced some `classical.decidable_eq` in lemma statements with instance parameters, because otherwise we have to use `congr` to apply these lemmas when a `decidable_eq` instance is available Additions: - `bilin_form.to_matrix` and `matrix.to_bilin`: given a basis, the equivalences between bilinear forms on any module and matrices - lemmas from `to_matrix'` and `to_bilin'` have been ported to `to_matrix` and `to_bilin` - `bilin_form.congr`, a dependency of `bilin_form.to_matrix`, states that `bilin_form R M` and `bilin_form R M'` are linearly equivalent if `M` and `M'` are - assorted lemmas involving `std_basis` Deletions: - `bilin_form.to_matrix_smul`: use `linear_equiv.map_smul` instead Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>