Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 23:41 cef5898c

View on Github →

chore(linear_algebra): generalize conversion between matrices and bilinear forms to semirings (#14263) Only one lemma was moved (dual_distrib_apply), none were renamed, and no proofs were meaningfully changed. Section markers were shuffled around, and some variables exchanged for variables with weaker typeclass assumptions. A few other things have been generalized to semiring at the same time; linear_map.trace and linear_map.smul_rightₗ

Estimated changes

modified theorem bilin_form.ext_basis
modified theorem basis.to_matrix_units_smul
modified theorem bilin_form.mul_to_matrix'
modified theorem bilin_form.mul_to_matrix
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_apply
modified theorem bilin_form.to_matrix_mul
modified def matrix.to_bilin'
modified theorem matrix.to_bilin'_apply'
modified theorem matrix.to_bilin'_apply
modified theorem matrix.to_bilin'_aux_eq
modified theorem matrix.to_bilin'_comp
modified theorem matrix.to_bilin'_std_basis
modified theorem matrix.to_bilin'_to_matrix'
modified theorem matrix.to_bilin_apply
modified theorem matrix.to_bilin_comp
modified theorem matrix.to_bilin_to_matrix
modified theorem to_bilin'_aux_to_matrix_aux