Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-21 21:43 5f517714

View on Github →

feat(linear_algebra/bilinear_form): basis changing bilin_form.to_matrix (#8775) A few simp lemmas on bilinear forms.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

added theorem bilin_form.comp_id_id

added theorem bilin_form.comp_id_left

added theorem bilin_form.comp_id_right

added theorem bilin_form.comp_left_id

added theorem bilin_form.comp_right_id

added theorem bilin_form.to_matrix_mul_basis_to_matrix