[Merged by Bors] - feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains by SnirBroshi · Pull Request #39634 · leanprover-community/mathlib4

SnirBroshi · 2026-05-20T23:35:31Z

Syntactically generalize the bilinear form identities to non-square matrices
Prove iff and transpose theorems for SeparatingLeft/SeparatingRight/Nondegenerate
Prove M *ᵥ v = 0 → v = 0 and v ᵥ* M = 0 → v = 0 given Nondegenerate
(extracted from the existing eq_zero_of_*_eq_zero)
Generalize M.det ≠ 0 → M.Nondegenerate to M.det ∈ R⁰ → M.Nondegenerate (over any CommRing)
Add M *ᵥ v = 0 → v = 0 and v ᵥ* M = 0 → v = 0 theorems given M.det ∈ R⁰
Allow NonUnitalNonAssocSemirings in the defs

…generate` to non-domains with `det ∈ nonZeroDivisors`

github-actions · 2026-05-20T23:36:50Z

PR summary d991d28488

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ Nondegenerate.of_det_mem_nonZeroDivisors
+ Nondegenerate.transpose
+ SeparatingLeft.eq_zero_of_vecMul_eq_zero
+ SeparatingLeft.nondegenerate
+ SeparatingLeft.of_det_mem_nonZeroDivisors
+ SeparatingLeft.separatingRight
+ SeparatingLeft.separatingRight_transpose
+ SeparatingRight.eq_zero_of_mulVec_eq_zero
+ SeparatingRight.nondegenerate
+ SeparatingRight.separatingLeft
+ SeparatingRight.separatingLeft_transpose
+ eq_zero_of_det_mem_nonZeroDivisors_of_mulVec_eq_zero
+ eq_zero_of_det_mem_nonZeroDivisors_of_vecMul_eq_zero
+ nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero
+ nondegenerate_iff_separatingLeft
+ nondegenerate_iff_separatingRight
+ nondegenerate_transpose_iff
+ separatingLeft_iff_forall_vecMul_eq_zero
+ separatingLeft_iff_separatingRight
+ separatingLeft_transpose_iff
+ separatingRight_iff_forall_mulVec_eq_zero
+ separatingRight_transpose_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit d991d28).

+22 new declarations
−0 removed declarations

+Matrix.Nondegenerate.of_det_mem_nonZeroDivisors
+Matrix.Nondegenerate.transpose
+Matrix.SeparatingLeft.eq_zero_of_vecMul_eq_zero
+Matrix.SeparatingLeft.nondegenerate
+Matrix.SeparatingLeft.separatingRight
+Matrix.SeparatingLeft.separatingRight_transpose
+Matrix.SeparatingRight.eq_zero_of_mulVec_eq_zero
+Matrix.SeparatingRight.nondegenerate
+Matrix.SeparatingRight.separatingLeft
+Matrix.SeparatingRight.separatingLeft_transpose
+Matrix.eq_zero_of_det_mem_nonZeroDivisors_of_mulVec_eq_zero
+Matrix.eq_zero_of_det_mem_nonZeroDivisors_of_vecMul_eq_zero
+Matrix.nondegenerate_iff
+Matrix.nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero
+Matrix.nondegenerate_iff_separatingLeft
+Matrix.nondegenerate_iff_separatingRight
+Matrix.nondegenerate_transpose_iff
+Matrix.separatingLeft_iff_forall_vecMul_eq_zero
+Matrix.separatingLeft_iff_separatingRight
+Matrix.separatingLeft_transpose_iff
+Matrix.separatingRight_iff_forall_mulVec_eq_zero
+Matrix.separatingRight_transpose_iff

No changes to strong technical debt.

No changes to weak technical debt.

Current commit d991d28488
Reference commit 2929a78989

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

… square matrices in domains

…id `classical`

…nzerodivisors

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

themathqueen

Thanks!

maintainer merge

github-actions · 2026-06-30T09:05:32Z

🚀 Pull request has been placed on the maintainer queue by themathqueen.

ocfnash · 2026-07-01T17:20:31Z

Thanks!

bors merge

…non-domains (#39634) - Syntactically generalize the bilinear form identities to non-square matrices - Prove iff and transpose theorems for `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` - Prove `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` given `Nondegenerate` (extracted from the existing `eq_zero_of_*_eq_zero`) - Generalize `M.det ≠ 0 → M.Nondegenerate` to `M.det ∈ R⁰ → M.Nondegenerate` (over any `CommRing`) - Add `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` theorems given `M.det ∈ R⁰` - Allow `NonUnitalNonAssocSemiring`s in the `def`s

mathlib-bors · 2026-07-01T18:31:37Z

Pull request successfully merged into master.

Build succeeded:

…emiring (#41271) This PR generalizes the `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` lemmas from `CommRing` to `CommSemiring` (the determinant section keeps `CommRing`), and golfs `nondegenerate_def` using the `@[mk_iff]`-generated `nondegenerate_iff`. Follow-up to #39634, which generalized the definitions but left the lemmas at `CommRing`. 🤖 Prepared with Claude Code

…non-domains (leanprover-community#39634) - Syntactically generalize the bilinear form identities to non-square matrices - Prove iff and transpose theorems for `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` - Prove `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` given `Nondegenerate` (extracted from the existing `eq_zero_of_*_eq_zero`) - Generalize `M.det ≠ 0 → M.Nondegenerate` to `M.det ∈ R⁰ → M.Nondegenerate` (over any `CommRing`) - Add `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` theorems given `M.det ∈ R⁰` - Allow `NonUnitalNonAssocSemiring`s in the `def`s

…emiring (leanprover-community#41271) This PR generalizes the `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` lemmas from `CommRing` to `CommSemiring` (the determinant section keeps `CommRing`), and golfs `nondegenerate_def` using the `@[mk_iff]`-generated `nondegenerate_iff`. Follow-up to leanprover-community#39634, which generalized the definitions but left the lemmas at `CommRing`. 🤖 Prepared with Claude Code

…non-domains (leanprover-community#39634) - Syntactically generalize the bilinear form identities to non-square matrices - Prove iff and transpose theorems for `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` - Prove `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` given `Nondegenerate` (extracted from the existing `eq_zero_of_*_eq_zero`) - Generalize `M.det ≠ 0 → M.Nondegenerate` to `M.det ∈ R⁰ → M.Nondegenerate` (over any `CommRing`) - Add `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` theorems given `M.det ∈ R⁰` - Allow `NonUnitalNonAssocSemiring`s in the `def`s

…emiring (leanprover-community#41271) This PR generalizes the `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` lemmas from `CommRing` to `CommSemiring` (the determinant section keeps `CommRing`), and golfs `nondegenerate_def` using the `@[mk_iff]`-generated `nondegenerate_iff`. Follow-up to leanprover-community#39634, which generalized the definitions but left the lemmas at `CommRing`. 🤖 Prepared with Claude Code

feat(LinearAlgebra/Matrix/Nondegenerate): generalize `det ≠ 0 → Nonde…

f4730bf

…generate` to non-domains with `det ∈ nonZeroDivisors`

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

SnirBroshi added 6 commits May 21, 2026 06:56

delete A and just use R

9b16f01

use nonZeroDivisors notation

d5aacdd

extract the argument for a Nondegenerate hypothesis

883dc1d

transpose theorems to make mulVec work

1239439

cleanup

0a987cd

generalize further

9717541

SnirBroshi changed the title ~~feat(LinearAlgebra/Matrix/Nondegenerate): generalize det ≠ 0 → Nondegenerate~~ feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains May 21, 2026

SnirBroshi added 2 commits May 21, 2026 19:07

cleanup

457f9d6

SeparatingLeft/SeparatingRight/Nondegenerate are equivalent for…

4f59719

… square matrices in domains

themathqueen reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean Outdated

themathqueen reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean Outdated

SnirBroshi added 3 commits May 21, 2026 22:54

generalize the definitions for good measure

fe40743

move classical closer to usage

06df011

variable ... in is silly

953df37

SnirBroshi requested a review from themathqueen May 21, 2026 22:48

themathqueen reviewed May 23, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

themathqueen reviewed May 23, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean Outdated

themathqueen reviewed May 23, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

SnirBroshi added 4 commits May 25, 2026 05:50

tag transpose lemmas as @[simp]

13cb34b

remove more variable ... in

7317b59

use the other theorems in separatingLeft_iff_separatingRight to avo…

8824264

…id `classical`

extract variables in ToLinearEquiv.lean

f195841

SnirBroshi requested a review from themathqueen May 25, 2026 03:00

themathqueen reviewed Jun 2, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean Outdated

themathqueen reviewed Jun 4, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

SnirBroshi added 2 commits June 7, 2026 03:17

Merge branch 'master' into feature/matrix/nondegenerate-generalize-no…

52a0560

…nzerodivisors

simpa using!

dae7377

SnirBroshi and others added 2 commits June 24, 2026 23:02

move open scoped

6775d92

golf *_iff_det_ne_zero

87f8a81

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 24, 2026

SnirBroshi requested a review from themathqueen June 24, 2026 20:09

mathlib-triage Bot assigned joelriou Jun 25, 2026

themathqueen reviewed Jun 25, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean Outdated

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean Outdated

themathqueen added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 25, 2026

reorder of_ hypotheses in names

92cd008

SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 25, 2026

SnirBroshi requested a review from themathqueen June 25, 2026 12:23

themathqueen reviewed Jun 29, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean Outdated

shorten rw to simp

d991d28

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

SnirBroshi requested a review from themathqueen June 29, 2026 14:42

themathqueen reviewed Jun 30, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 30, 2026

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jul 1, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 1, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jul 1, 2026

mathlib-bors Bot changed the title ~~feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains~~ [Merged by Bors] - feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains Jul 1, 2026

mathlib-bors Bot closed this Jul 1, 2026

kim-em mentioned this pull request Jul 2, 2026

[Merged by Bors] - chore(LinearAlgebra/Matrix/Nondegenerate): generalize lemmas to CommSemiring #41271

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains#39634

[Merged by Bors] - feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains#39634
SnirBroshi wants to merge 27 commits into
leanprover-community:masterfrom
SnirBroshi:feature/matrix/nondegenerate-generalize-nonzerodivisors

SnirBroshi commented May 20, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 20, 2026 •

edited

Loading

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

ocfnash commented Jul 1, 2026

Uh oh!

mathlib-bors Bot commented Jul 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary d991d28488

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

ocfnash commented Jul 1, 2026

Uh oh!

mathlib-bors Bot commented Jul 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

SnirBroshi commented May 20, 2026 •

edited

Loading

github-actions Bot commented May 20, 2026 •

edited

Loading