Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-23 17:02 96a20388

View on Github →

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

Estimated changes

modified theorem alt_bilin_form.neg
modified def bilin_form.comp
modified theorem bilin_form.comp_apply
modified theorem bilin_form.comp_injective
modified theorem bilin_form.ext
modified theorem bilin_form.lin_mul_lin_comp
deleted theorem bilin_form.map_sum_left
deleted theorem bilin_form.map_sum_right
modified theorem bilin_form.mul_to_matrix
modified theorem bilin_form.neg_apply
modified theorem bilin_form.neg_left
modified theorem bilin_form.neg_right
modified theorem bilin_form.ortho_zero
modified theorem bilin_form.smul_apply
modified theorem bilin_form.sub_left
modified theorem bilin_form.sub_right
added theorem bilin_form.to_lin_symm
modified def bilin_form.to_matrix
modified theorem bilin_form.to_matrix_apply
modified theorem bilin_form.to_matrix_comp
modified theorem bilin_form.to_matrix_mul
modified theorem bilin_form.to_matrix_smul
modified theorem bilin_form.zero_left
modified theorem bilin_form.zero_right
modified structure bilin_form
modified def linear_map.to_bilin
added theorem map_sum_left
added theorem map_sum_right
modified def matrix.to_bilin_form
modified theorem matrix.to_bilin_form_apply
modified theorem to_bilin_form_to_matrix
added theorem to_linear_map_apply
modified theorem to_matrix_to_bilin_form