feat(LinearAlgebra/Matrix/MoorePenrose): define the Moore-Penrose pseudo-inverse by KryptosAI · Pull Request #36889 · leanprover-community/mathlib4

KryptosAI · 2026-03-20T05:48:55Z

Defines IsMoorePenroseInverse and constructs the Moore-Penrose pseudo-inverse for matrices over RCLike fields. Closes #24787.

Defs.lean defines the predicate using the heterogeneous four-condition characterization from the issue, plus uniqueness for semigroups with StarMul.

Basic.lean constructs the inverse via orthogonal projection and ker(f)ᗮ ≃ₗ range(f), then proves:

theorem exists_isMoorePenroseInverse (A : Matrix m n 𝕜) :
    ∃ (As : Matrix n m 𝕜), IsMoorePenroseInverse A As

def moorePenroseInverse (A : Matrix m n 𝕜) : Matrix n m 𝕜

lemma moorePenroseInverse_conjTranspose :
    moorePenroseInverse (Aᴴ) = (moorePenroseInverse A)ᴴ

lemma moorePenroseInverse_eq_nonsing_inv (hA : IsUnit A) :
    moorePenroseInverse A = A⁻¹

AI disclosure

Gemini 2.5 Pro: proof planning, initial code, edits
Claude Code (Opus 4.6): debugging, compilation, type-checking against mathlib4

I reviewed and directed all changes.

github-actions · 2026-03-20T05:49:06Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-03-20T05:50:10Z

PR summary 6ef8cc2731

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.Matrix.MoorePenrose.Defs` (new file)	496
`Mathlib.LinearAlgebra.Matrix.MoorePenrose.Basic` (new file)	2145

Declarations diff

+ IsMoorePenroseInverse
+ _root_.IsMoorePenroseInverse.eq_moorePenroseInverse
+ exists_isMoorePenroseInverse
+ isMoorePenroseInverse_moorePenroseInverse
+ isMoorePenroseInverse_unique
+ isSelfAdjoint_mul
+ isSelfAdjoint_mul'
+ moorePenroseInverse
+ moorePenroseInverse_conjTranspose
+ moorePenroseInverse_eq_nonsing_inv
+ moorePenroseInverse_moorePenroseInverse
+ moorePenroseInverse_mul_self_mul
+ moorePenroseInverse_one
+ moorePenroseInverse_zero
+ mul_moorePenroseInverse_mul
+ star_moorePenroseInverse_mul
+ star_mul_moorePenroseInverse
+ symm
+ unique

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

…udo-inverse Co-Authored-By: Claude Opus 4.6 <[email protected]>

vihdzp

Unfamiliar with the mathematics, my comments are mostly stylistic.

vihdzp · 2026-03-20T08:38:02Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Defs.lean

+
+## References
+
+* <https://github.com/leanprover-community/mathlib4/issues/24787>


We probably don't want to cite ourselves.

Suggested change

* <https://github.com/leanprover-community/mathlib4/issues/24787>

Done, removed.

vihdzp · 2026-03-20T08:38:25Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Defs.lean

+2. `As * A * As = As`
+3. `A * As` is self-adjoint (`star (A * As) = A * As`)
+4. `As * A` is self-adjoint (`star (As * A) = As * A`) -/
+def IsMoorePenroseInverse {α β γ δ} [HMul α β γ] [HMul β α δ] [HMul γ α α]


Can we make this into a structure, so we can give names to the four conditions?

Done — converted to a structure with named fields. Also added attribute [simp] on all four projections and updated symm to use where syntax.

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

vihdzp · 2026-03-20T08:39:47Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+
+## References
+
+* <https://github.com/leanprover-community/mathlib4/issues/24787>


Suggested change

* <https://github.com/leanprover-community/mathlib4/issues/24787>

vihdzp · 2026-03-20T08:40:32Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+import Mathlib.LinearAlgebra.Matrix.MoorePenrose.Defs
+
+/-!
+# The Moore-Penrose Pseudo-Inverse for Matrices


Suggested change

# The Moore-Penrose Pseudo-Inverse for Matrices

# The Moore-Penrose pseudo-inverse for matrices

vihdzp · 2026-03-20T08:42:34Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+    Kᗮ.subtype ∘ₗ e.symm.toLinearMap ∘ₗ
+      (Submodule.orthogonalProjection W : _ →L[𝕜] _).toLinearMap
+  let As : Matrix n m 𝕜 :=
+    (Matrix.toEuclideanLin (𝕜 := 𝕜) (m := n) (n := m)).symm g


Why not use this as the definition, instead of extracting this out with choice?

Good call — moorePenroseInverse now uses the explicit construction directly. exists_isMoorePenroseInverse is a trivial corollary.

vihdzp · 2026-03-20T08:42:44Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+The construction uses the restricted isomorphism `ker(f)ᗮ ≃ₗ range(f)`
+and orthogonal projections. -/
+theorem exists_isMoorePenroseInverse (A : Matrix m n 𝕜) :
+    ∃ (As : Matrix n m 𝕜), IsMoorePenroseInverse A As := by


Suggested change

∃ (As : Matrix n m 𝕜), IsMoorePenroseInverse A As := by

∃ As : Matrix n m 𝕜, IsMoorePenroseInverse A As := by

vihdzp · 2026-03-20T08:44:56Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+  (exists_isMoorePenroseInverse A).choose_spec
+
+@[simp]
+lemma moorePenroseInverse_zero : moorePenroseInverse (0 : Matrix m n 𝕜) = 0 := by


Might be worth having a IsMoorePenroseInverse.eq lemma stating IsMoorePenroseInverse A B → moorePenroseInverse A = B .

Added as IsMoorePenroseInverse.eq_moorePenroseInverse. Used it to simplify moorePenroseInverse_zero, moorePenroseInverse_one, moorePenroseInverse_moorePenroseInverse, moorePenroseInverse_conjTranspose, and moorePenroseInverse_eq_nonsing_inv.

vihdzp · 2026-03-20T08:50:12Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+  apply isMoorePenroseInverse_unique (isMoorePenroseInverse_moorePenroseInverse 1)
+  exact ⟨by simp, by simp, by simp, by simp⟩
+
+/-- The four Penrose conditions hold for `A` and `moorePenroseInverse A`. -/


Seems weird to only comment this on the first one. I think the easiest way to fix this is to just remove the remark.

Done, removed.

- Convert `IsMoorePenroseInverse` from a conjunction to a structure with named fields for the four Penrose conditions. - Define `moorePenroseInverse` via the explicit construction instead of `Classical.choose`. - Add `IsMoorePenroseInverse.eq_moorePenroseInverse` convenience lemma. - Remove self-citation from references, fix module doc, style fixes. Co-Authored-By: Claude Opus 4.6 <[email protected]>

Co-Authored-By: Claude Opus 4.6 <[email protected]>

KryptosAI · 2026-03-20T15:37:05Z

thank you so much for the review! i think all have been addressed now.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

eric-wieser · 2026-04-01T16:27:42Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

+/-- Heterogeneous uniqueness for matrices. -/
+lemma isMoorePenroseInverse_unique {A : Matrix m n 𝕜} {B C : Matrix n m 𝕜}
+    (hB : IsMoorePenroseInverse A B) (hC : IsMoorePenroseInverse A C) : B = C := by


Isn't this a duplicate of a lemma you wrote in the other file?

Not quite: IsMoorePenroseInverse.unique in Defs is the homogeneous semigroup lemma, so for matrices it only covers the square case where A, B, and C all have the same type. This lemma is the rectangular Matrix m n / Matrix n m specialization. I added a short note in e1939ce to make that distinction explicit.

themathqueen · 2026-04-04T17:26:01Z

Mathlib/LinearAlgebra/Matrix/MoorePenrose/Basic.lean

This probably belongs in Analysis/Matrix since it import analysis stuff.

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 20, 2026

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 20, 2026

KryptosAI force-pushed the feat/moore-penrose-inverse branch from d3c3c79 to bb46eca Compare March 20, 2026 05:54

feat(LinearAlgebra/Matrix/MoorePenrose): define the Moore-Penrose pse…

1f2d10b

…udo-inverse Co-Authored-By: Claude Opus 4.6 <[email protected]>

KryptosAI force-pushed the feat/moore-penrose-inverse branch from bb46eca to 1f2d10b Compare March 20, 2026 05:57

robin-carlier added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 20, 2026

vihdzp reviewed Mar 20, 2026

View reviewed changes

KryptosAI and others added 2 commits March 20, 2026 08:24

chore: fix copyright year and header casing

b76fa9b

Co-Authored-By: Claude Opus 4.6 <[email protected]>

KryptosAI and others added 2 commits March 21, 2026 00:32

chore: add module declarations for Lean 4.29 compatibility

7f1234e

Co-Authored-By: Claude Opus 4.6 <[email protected]>

chore: add @[expose] public section for module visibility

71767bf

Co-Authored-By: Claude Opus 4.6 <[email protected]>

mathlib-triage bot assigned dagurtomas Mar 27, 2026

dagurtomas removed their assignment Apr 1, 2026

dagurtomas requested a review from eric-wieser April 1, 2026 16:01

eric-wieser reviewed Apr 1, 2026

View reviewed changes

mathlib-triage bot assigned ocfnash Apr 2, 2026

KryptosAI added 2 commits April 1, 2026 18:32

docs: clarify rectangular uniqueness lemma

e1939ce

Merge branch 'master' into feat/moore-penrose-inverse

95700e1

themathqueen reviewed Apr 4, 2026

View reviewed changes


		## References

		* <https://github.com/leanprover-community/mathlib4/issues/24787>

	# The Moore-Penrose Pseudo-Inverse for Matrices
	# The Moore-Penrose pseudo-inverse for matrices

	∃ (As : Matrix n m 𝕜), IsMoorePenroseInverse A As := by
	∃ As : Matrix n m 𝕜, IsMoorePenroseInverse A As := by

Conversation

KryptosAI commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

AI disclosure

Uh oh!

github-actions bot commented Mar 20, 2026

Welcome new contributor!

Uh oh!

github-actions bot commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 6ef8cc2731

Import changes for modified files

Declarations diff

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

KryptosAI commented Mar 20, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

KryptosAI commented Mar 20, 2026 •

edited

Loading

github-actions bot commented Mar 20, 2026 •

edited

Loading