# Commit 2020-11-27 09:16 d0789503

View on Github →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