Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added theorem bilin_form.comp_comp
added theorem bilin_form.comp_congr
added def bilin_form.congr
added theorem bilin_form.congr_apply
added theorem bilin_form.congr_comp
added theorem bilin_form.congr_symm
added theorem bilin_form.ext_basis
modified theorem bilin_form.mul_to_matrix
modified theorem bilin_form.to_matrix_apply
modified theorem bilin_form.to_matrix_comp
modified theorem bilin_form.to_matrix_mul
deleted theorem bilin_form.to_matrix_smul
added def matrix.to_bilin'
added theorem matrix.to_bilin'_apply
added theorem matrix.to_bilin'_comp
added theorem matrix.to_bilin'_symm
added theorem matrix.to_bilin_apply
added theorem matrix.to_bilin_comp
deleted theorem matrix.to_bilin_form_comp
added theorem matrix.to_bilin_symm
deleted theorem to_bilin_form_to_matrix
deleted theorem to_matrix_to_bilin_form