Commit 2020-11-27 09:16 d0789503

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