feat(InnerProductSpace/PiL2): det of a linear isometry has unit norm by jayscambler · Pull Request #39192 · leanprover-community/mathlib4

jayscambler · 2026-05-11T11:50:03Z

Adds LinearIsometryEquiv.norm_det and the real corollary LinearIsometryEquiv.abs_det. The proof uses the unitary matrix of a linear isometry in orthonormal bases, via LinearIsometryEquiv.toMatrix_mem_unitaryGroup and Matrix.det_of_mem_unitary. The supporting matrix lemma is moved from Adjoint.lean to PiL2.lean, where it no longer depends on adjoints.

For a linear isometry equivalence `R : E ≃ₗᵢ[𝕜] E` of a finite-dimensional inner-product space, the determinant of the underlying linear map has unit norm. This is the natural endomorphism counterpart to `OrthonormalBasis.det_to_matrix_orthonormalBasis : ‖a.toBasis.det b‖ = 1` (already in mathlib). The proof routes through that lemma by expressing `R` as the change-of-basis matrix between `b` and `b.map R` in any orthonormal basis. New lemmas: - `LinearIsometryEquiv.norm_det` (`@[simp]`): the RCLike-generic form. - `LinearIsometryEquiv.abs_det` (`@[simp]`): the real-specific corollary via `Real.norm_eq_abs`. Use case: combined with `Measure.addHaar_preimage_continuousLinearEquiv`, this gives `volume (R⁻¹' T) = volume T` for any set `T` (no measurability needed) on `EuclideanSpace ℝ (Fin n)`.

github-actions · 2026-05-11T11:50:20Z

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-05-11T11:51:15Z

PR summary f40a8e8c6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ abs_det
+ norm_det

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.

No changes to strong technical debt.

No changes to weak technical debt.

wwylele

According to the guideline, could you disclose your usage of AI, if any?

The PR description is suspiciously verbose and it looks like AI-written, which would be prohibited by the guideline. Or perhaps you unfortunately copied the format from other AI-generated PR. In any case, could you make it concise?

wwylele · 2026-05-11T14:30:03Z

+theorem norm_det (R : E ≃ₗᵢ[𝕜] E) :
+    ‖LinearMap.det (R : E →ₗ[𝕜] E)‖ = 1 := by


Here is a shorter proof

theorem norm_det (R : E ≃ₗᵢ[𝕜] E) : ‖R.toLinearMap.det‖ = 1 := by rw [← R.toLinearMap.det_toMatrix (stdOrthonormalBasis 𝕜 E).toBasis] apply CStarRing.norm_of_mem_unitary exact Matrix.det_of_mem_unitary <| R.toMatrix_mem_unitaryGroup _ _

wwylele · 2026-05-11T14:36:27Z

+  have h : ‖LinearMap.det (R : F' →ₗ[ℝ] F')‖ = 1 := norm_det (𝕜 := ℝ) (E := F') R
+  rwa [Real.norm_eq_abs] at h


does this work?

Suggested change

have h : ‖LinearMap.det (R : F' →ₗ[ℝ] F')‖ = 1 := norm_det (𝕜 := ℝ) (E := F') R

rwa [Real.norm_eq_abs] at h

simpa using R.norm_det

jayscambler · 2026-05-11T17:04:21Z

Thanks. To disclose: an initial proof and the original PR draft were produced in collaboration with Claude Opus 4.7 (Anthropic) while testing Grey Haven's autocontext tool on a longer-running Lean formalization (Putnam 2013 A5). I read every line, ran lake build against master locally before submitting, and am opening this PR myself. Given the experimental nature of the workflow, I'd particularly welcome review feedback on any aspect of the proof or naming.

On the shorter proof: going to try the refactor (moving LinearIsometryEquiv.toMatrix_mem_unitaryGroup so it's available from PiL2.lean) and will report back. Also rewriting the PR description more concisely.

@wwylele

Move `LinearIsometryEquiv.toMatrix_mem_unitaryGroup` from `Adjoint.lean` up to `PiL2.lean` so it is in scope where `norm_det` is stated. The new proof in `PiL2.lean` does not go through `adjoint`; instead it reduces to `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` via `b.map f`. With the lemma available, `norm_det` becomes the three-line form @wwylele suggested.

The previous refactor commit deleted the final theorem in the file but left a trailing blank line, which the `end-of-file-fixer` pre-commit hook flagged in CI.

Use `simpa only [Real.norm_eq_abs] using R.norm_det` instead of the two-line have/rwa version. Suggested by reviewer.

grunweg · 2026-05-11T18:43:37Z

Moderation note: per mathlib's contribution guidelines, LLM-written comments on github are not allowed. Your comment looks very LLM-generated. Please write comments by hand in the future.

Consider this as official warning.

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 May 11, 2026

github-actions Bot added the t-analysis Analysis (normed *, calculus) label May 11, 2026

wwylele reviewed May 11, 2026

View reviewed changes

jayscambler force-pushed the feat/linearIsometryEquiv-abs-det branch from ad19edb to 263f08b Compare May 11, 2026 17:04

This comment was marked as low quality.

Sign in to view

jayscambler added 2 commits May 11, 2026 12:15

chore: strip trailing blank line in Adjoint.lean

6b0e584

The previous refactor commit deleted the final theorem in the file but left a trailing blank line, which the `end-of-file-fixer` pre-commit hook flagged in CI.

refactor(InnerProductSpace/PiL2): simplify abs_det proof

a2a47b6

Use `simpa only [Real.norm_eq_abs] using R.norm_det` instead of the two-line have/rwa version. Suggested by reviewer.

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label May 11, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(InnerProductSpace/PiL2): det of a linear isometry has unit norm#39192

feat(InnerProductSpace/PiL2): det of a linear isometry has unit norm#39192
jayscambler wants to merge 4 commits into
leanprover-community:masterfrom
greyhaven-ai:feat/linearIsometryEquiv-abs-det

jayscambler commented May 11, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 11, 2026

Uh oh!

github-actions Bot commented May 11, 2026 •

edited

Loading

Declarations diff

Uh oh!

wwylele left a comment

Uh oh!

wwylele May 11, 2026 •

edited

Loading

Uh oh!

wwylele May 11, 2026

Uh oh!

jayscambler commented May 11, 2026

Uh oh!

This comment was marked as low quality.

grunweg commented May 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		theorem norm_det (R : E ≃ₗᵢ[𝕜] E) :
		‖LinearMap.det (R : E →ₗ[𝕜] E)‖ = 1 := by

		have h : ‖LinearMap.det (R : F' →ₗ[ℝ] F')‖ = 1 := norm_det (𝕜 := ℝ) (E := F') R
		rwa [Real.norm_eq_abs] at h

	have h : ‖LinearMap.det (R : F' →ₗ[ℝ] F')‖ = 1 := norm_det (𝕜 := ℝ) (E := F') R
	rwa [Real.norm_eq_abs] at h
	simpa using R.norm_det

Conversation

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

Uh oh!

Uh oh!

github-actions Bot commented May 11, 2026

Welcome new contributor!

Uh oh!

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

Uh oh!

PR summary f40a8e8c6e

Import changes for modified files

Declarations diff

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele May 11, 2026

Choose a reason for hiding this comment

Uh oh!

jayscambler commented May 11, 2026

Uh oh!

This comment was marked as low quality.

grunweg commented May 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jayscambler commented May 11, 2026 •

edited

Loading

github-actions Bot commented May 11, 2026 •

edited

Loading

wwylele May 11, 2026 •

edited

Loading