Revision #3237 → #3779 · back to history
addedDeterminant of a matrix45fe814d0b4f
addedElementary matrix (transvection)8910d14ee21d
addedAdjugate matrixc8d4f958ab6b
modifiedSchur complementfce66cdf6cae
| Field | From #3237 | To #3779 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.Matrix.SchurComplement | Mathlib.Data.Matrix.Block |
| note | The Schur complement `D - C A⁻¹ B` appears throughout `Mathlib.LinearAlgebra.Matrix.SchurComplement` in lemmas like `Matrix.fromBlocks_eq_of_invertible_top_left` and `Matrix.det_fromBlocks₁₁`. | The Schur complement `D - C A⁻¹ B` appears throughout `Mathlib.LinearAlgebra.Matrix.SchurComplement` in lemmas like `Matrix.fromBlocks_eq_of_invertible_top_left` and `Matrix.det_fromBlocks₁₁`, built on `Matrix.fromBlocks` from `Mathlib.Data.Matrix.Block`. |
addedInvertible iff full rankdf11f8a61b8c
modifiedInvertible iff trivial kernelec7164d0b30b
| Field | From #3237 | To #3779 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.Basic | Mathlib.Algebra.Module.Submodule.Ker |
modifiedInvertible matrix is product of elementary matricesb5462efbcab9
| Field | From #3237 | To #3779 |
|---|
| mathlib.decl | — | Matrix.diagonal_transvection_induction_of_det_ne_zero |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.Matrix.Transvection |
| note | Mathlib defines `Matrix.TransvectionStruct` and proves every invertible matrix is a product of diagonal and transvection matrices (`diagonal_transvection_induction`), but no statement in terms of generic elementary matrices. | Mathlib defines `Matrix.TransvectionStruct` and proves every invertible matrix is a product of diagonal and transvection matrices (`diagonal_transvection_induction_of_det_ne_zero`), but no statement in terms of generic elementary matrices. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
modifiedRows of inverse orthonormal to columns534eb6430ac0
| Field | From #3237 | To #3779 |
|---|
| note | No statement framing the rows of `A⁻¹` as biorthogonal to the columns of `A` is in Mathlib. | No statement framing the rows of `A⁻¹` as biorthogonal to the columns of `A` is in Mathlib. (Note: the source's word `orthonormal` here is a misnomer for `biorthogonal` — the pairing yields Kronecker deltas via `UV = I`, not an orthonormality condition.) |
modifiedOne-sided inverse implies two-sided11eaf6802719
| Field | From #3237 | To #3779 |
|---|
| moderation_proposal.fields | — | {"mathlib":{"decl":"mul_eq_one_comm","module":"Mathlib.Algebra.Group.Monoid","match_kind":"generalization"}} |
| moderation_proposal.reason | — | `mul_eq_one_comm` lives in `Mathlib.Algebra.Group.Monoid` (general `MulOne`/`IsDedekindFiniteMonoid`); the cited module `Mathlib.LinearAlgebra.Matrix.SemiringInverse` does not contain a declaration named `mul_eq_one_comm`. |
addedLU decomposition3440aa149a8f