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