Skip to content

feat(LinearAlgebra/Matrix): add Sherman-Morrison formula#34875

Open
banrovegrie wants to merge 4 commits intoleanprover-community:masterfrom
banrovegrie:sherman-morrison
Open

feat(LinearAlgebra/Matrix): add Sherman-Morrison formula#34875
banrovegrie wants to merge 4 commits intoleanprover-community:masterfrom
banrovegrie:sherman-morrison

Conversation

@banrovegrie
Copy link
Copy Markdown

@banrovegrie banrovegrie commented Feb 5, 2026 •
edited
Loading

Mathlib has the matrix determinant lemma (det_add_replicateCol_mul_replicateRow in SchurComplement.lean) but lacked the corresponding inverse formula. This PR fills that gap.

  • Add Matrix.inv_add_vecMulVec: Sherman-Morrison formula for (A + uv^T)^{-1}
  • Add Matrix.inv_sub_vecMulVec: subtraction variant
  • Add Matrix.isUnit_det_add_vecMulVec: invertibility under the formula's hypotheses

Test plan

  • lake build passes
  • Lines within 100 char limit
  • All declarations have docstrings

@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Feb 5, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 5, 2026 •
edited
Loading

PR summary 5bad60a0ca

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.LinearAlgebra.Matrix.ShermanMorrison (new file) 1453

Declarations diff

+ inv_add_replicateCol_mul_replicateRow
+ inv_add_vecMulVec
+ inv_sub_vecMulVec
+ isUnit_det_add_vecMulVec
+ isUnit_det_sub_vecMulVec

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 5, 2026 •
edited
Loading

I think there's a shorter proof here along the lines of https://github.com/eric-wieser/lean-matrix-cookbook/blob/5682ac96f54bd119bd92b053962433c6940b6385/MatrixCookbook/3Inverses.lean#L131-L151

@banrovegrie
Copy link
Copy Markdown
Author

banrovegrie commented Feb 5, 2026

Hey @eric-wieser, thanks for pointing me to your lean-matrix-cookbook proof!

I've reworked it to follow your approach:
Woodbury $\to$ associativity rewrites $\to$ smul_eq_mul_diagonal + inv_subsingleton to pull out the scalar.

A few questions:

  • Does the proof structure look reasonable to you now?
  • I kept both the replicateCol/replicateRow form and the vecMulVec form in the API.
  • Any other simplifications you'd suggest?

@Shreyas4991 Shreyas4991 requested a review from Copilot February 7, 2026 05:47
Copilot AI reviewed Feb 7, 2026
View reviewed changes
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR adds Sherman–Morrison-style inverse and invertibility lemmas for rank-1 matrix updates to Mathlib’s matrix library, complementing the existing determinant lemma in SchurComplement.lean.

Changes:

  • Added Matrix.inv_add_vecMulVec and Matrix.inv_sub_vecMulVec, giving inverse formulas for A ± vecMulVec u v under the standard Sherman–Morrison hypotheses.
  • Added Matrix.isUnit_det_add_vecMulVec, providing an invertibility/isUnit determinant result for the rank-1 update.
  • Registered the new module via public import in Mathlib.lean.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File Description
Mathlib/LinearAlgebra/Matrix/ShermanMorrison.lean Introduces Sherman–Morrison inverse lemmas (add/sub variants) and an IsUnit determinant corollary.
Mathlib.lean Exposes the new Sherman–Morrison module through a top-level public import.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@wwylele
Copy link
Copy Markdown
Collaborator

wwylele commented Mar 1, 2026

The CI failed for possibly unrelated error. You probably want to merge master to retry CI again

@mathlib-triage mathlib-triage bot assigned eric-wieser and unassigned kim-em Mar 22, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot Copilot left review comments

+1 more reviewer

@Xxxjdjdid Xxxjdjdid Xxxjdjdid approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@eric-wieser eric-wieser

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@banrovegrie @eric-wieser @wwylele @Xxxjdjdid @kim-em