Revision #1254 → #2578 · back to history
modifiedGaussian eliminationd066cdee8e39
| Field | From #1254 | To #2578 |
|---|
| mathlib.decl | Matrix.exists_list_transvec_mul_diagonal_mul_list_transvec | Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec |
| provenance | ai | ai-moderated |
modifiedRow reduction as matrix decomposition413626076c35
| Field | From #1254 | To #2578 |
|---|
| mathlib.decl | Matrix.exists_list_transvec_mul_diagonal_mul_list_transvec | Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec |
| provenance | ai | ai-moderated |
modifiedGaussian elimination over any field15cab32f84b0
| Field | From #1254 | To #2578 |
|---|
| mathlib.decl | Matrix.exists_list_transvec_mul_mul_list_transvec_eq_diagonal | Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal |
| provenance | ai | ai-moderated |