Theorem Matrix.schur_complement_eq₂₂

Modification history

2025-09-25 08:21

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

refactor(LinearAlgebra/Matrix): move lemmas around to reduce imports (#29709) …

Modified Matrix.schur_complement_eq₂₂ View on Github →

2023-07-06 04:32

Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

feat: port LinearAlgebra.Matrix.SchurComplement (#5491)

Added Matrix.schur_complement_eq₂₂ View on Github →