Commit 2023-07-06 04:32 7e61a1a5

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

added theorem Matrix.IsHermitian.fromBlocks₁₁

added theorem Matrix.IsHermitian.fromBlocks₂₂

added theorem Matrix.PosSemidef.fromBlocks₁₁

added theorem Matrix.PosSemidef.fromBlocks₂₂

added theorem Matrix.det_fromBlocks_one₁₁

added theorem Matrix.det_fromBlocks_one₂₂

added theorem Matrix.det_fromBlocks₁₁

added theorem Matrix.det_fromBlocks₂₂

added theorem Matrix.det_mul_add_one_comm

added theorem Matrix.det_one_add_col_mul_row

added theorem Matrix.det_one_add_mul_comm

added theorem Matrix.det_one_sub_mul_comm

added def Matrix.fromBlocksZero₁₂Invertible

added def Matrix.fromBlocksZero₁₂InvertibleEquiv

added def Matrix.fromBlocksZero₂₁Invertible

added def Matrix.fromBlocksZero₂₁InvertibleEquiv

added theorem Matrix.fromBlocks_eq_of_invertible₁₁

added theorem Matrix.fromBlocks_eq_of_invertible₂₂

added def Matrix.fromBlocks₁₁Invertible

added def Matrix.fromBlocks₂₂Invertible

added theorem Matrix.invOf_fromBlocks_zero₁₂_eq

added theorem Matrix.invOf_fromBlocks_zero₂₁_eq

added theorem Matrix.invOf_fromBlocks₁₁_eq

added theorem Matrix.invOf_fromBlocks₂₂_eq

added theorem Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff

added theorem Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff

added def Matrix.invertibleEquivFromBlocks₁₁Invertible

added def Matrix.invertibleEquivFromBlocks₂₂Invertible

added def Matrix.invertibleOfFromBlocksZero₁₂Invertible

added def Matrix.invertibleOfFromBlocksZero₂₁Invertible

added def Matrix.invertibleOfFromBlocks₁₁Invertible

added def Matrix.invertibleOfFromBlocks₂₂Invertible

added theorem Matrix.isUnit_fromBlocks_iff_of_invertible₁₁

added theorem Matrix.isUnit_fromBlocks_iff_of_invertible₂₂

added theorem Matrix.isUnit_fromBlocks_zero₁₂

added theorem Matrix.isUnit_fromBlocks_zero₂₁

added theorem Matrix.schur_complement_eq₁₁

added theorem Matrix.schur_complement_eq₂₂