Revision #2997 → #3540 · back to history
4b8486b36a59| Field | From #2997 | To #3540 |
|---|---|---|
| mathlib.decl | Matrix.exists_list_transvec_mul_diagonal_mul_list_transvec | Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec |
| note | Mathlib formalizes Gaussian-elimination-style reductions via transvection decompositions and row echelon reductions on matrices. | Any matrix is a product of transvections, a diagonal matrix, and transvections — the Mathlib formalization of Gaussian elimination via elementary row/column operations. |
58d2c1e9cc83de1d4c1bda89b2f73d30d51a