feat(LinearAlgebra/Matrix/SchurComplement): rank-one determinant formula det(1 - φ•c) = 1 - φ c - #43776

feat(LinearAlgebra/Matrix/SchurComplement): rank-one determinant formula det(1 - φ•c) = 1 - φ c#43776

tobias-weiss-ai-xr wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

tobias-weiss-ai-xr:det-one-sub-smulrighttobias-weiss-ai-xr/mathlib4:det-one-sub-smulrightCopy head branch name to clipboard