[Merged by Bors] - fix: remove defeq abuse in the Hahn-Banach theorem#34530
Closed
j-loreaux wants to merge 1 commit intoleanprover-community:masterfrom
Closed
[Merged by Bors] - fix: remove defeq abuse in the Hahn-Banach theorem#34530j-loreaux wants to merge 1 commit intoleanprover-community:masterfrom
j-loreaux wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
PR summary 1ad113ee44Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 Decrease in tech debt: (relative, absolute) = (3.00, 0.00)
Current commit 1796b8fc3a You can run this locally as
|
j-loreaux
added
the
tech debt
1 task
Ruben-VandeVelde
approved these changes
Jan 28, 2026
Contributor
Ruben-VandeVelde
left a comment
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
ghost
added
the
maintainer-merge
ghost
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 29, 2026
This removes some `erw`s in the proof of the Hahn-Banach theorem by using `ContinuousLinearMap.extendTo𝕜'` instead of the unprimed version. While the diff adds a type ascription to the `hextends` argument in an `obtain`, so that it elaborates as `∀ x : p, g ↑x = fr x` instead of `∀ x : p.restrictScalars ℝ, g ↑x = fr x`, this is in fact helping to *avoid* defeq abuse (since the domain of `fr` is `↥p` not `↥(p.restrictScalars ℝ)`).
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
YellPika
pushed a commit
to YellPika/mathlib4
that referenced
this pull request
Feb 3, 2026
…ity#34530) This removes some `erw`s in the proof of the Hahn-Banach theorem by using `ContinuousLinearMap.extendTo𝕜'` instead of the unprimed version. While the diff adds a type ascription to the `hextends` argument in an `obtain`, so that it elaborates as `∀ x : p, g ↑x = fr x` instead of `∀ x : p.restrictScalars ℝ, g ↑x = fr x`, this is in fact helping to *avoid* defeq abuse (since the domain of `fr` is `↥p` not `↥(p.restrictScalars ℝ)`).
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 25, 2026
) This PR concerns the extension of `ℝ`-linear (continuous or not) functionals to `𝕜`-linear functionals. This does several things, but I felt it was better to do it all at once, rather than having repeated churn in the same files because the current setup is a mess for numerous reasons. Unfortunately, that means the diff is a bit of a mess; I think the easiest way to review this PR is read the following discussion and then only look at the *new* code (and check that the deprecations exist). I will begin by highlighting the current problems: 1. Naming: the primary declarations `LinearMap.extendTo𝕜'` and `ContinuousLinearMap.extendTo𝕜'` are in the wrong namespaces (`Module.Dual` and `StrongDual`), and contain a variable name `𝕜`. 2. These declarations are primed, and their unprimed counterparts operate directly on `RestrictScalars`. This is nominally (according to the module documentation) for convenience, but it leads to defeq abuse (see #34530) and so should be avoided anyway. That PR removes the only occurrence of the use of the unprimed declarations in Mathlib. 3. The declaration `ContinuousLinearMap.extendTo𝕜'` has type class assumptions (normed ones) that are too strong, thereby making it unusable for non-normed spaces (e.g., when one wants to consider continuous linear functionals on the weak dual of a Banach space). 4. Point (3) led to the creation of `RCLike.extendTo𝕜'ₗ` which is just `ContinuousLinearMap.extendTo𝕜'` except reproven with weaker type class assumptions and bundled into a linear map. 5. There are missing `simp` lemmas, namely, ones concerning the imaginary part of the extension applied to a vector. 6. We're missing appropriately bundled versions, with `RCLike.extendTo𝕜'ₗ` being the only bundling currently. In this PR: we fix the above by doing the following: 1. Renaming `LinearMap.extendTo𝕜'` → `Module.Dual.extendRCLike` and `ContinuousLinearMap.extendTo𝕜'` → `StrongDual.extendRCLike`. 2. Removing the unprimed counterparts that operate on `RestrictScalars` 3. Weakening the type class assumptions on the newly renamed `StrongDual.extendRCLike` 4. Move `RCLike.extendTo𝕜'ₗ` out of its current location (`Analysis/LocallyConvex/Separation`) and next to `StrongDual.extendRCLike`; use the newly generalized `StrongDual.extendRCLike` to define it; rename it to `StrongDual.extendRCLikeₗ`; upgrade it from a linear map to a linear equivalence. 5. Add the missing simp lemmas for imaginary parts. 6. Add other appropriate bundlings, namely `Module.Dual.extendRCLikeₗ : Dual E ℝ ≃ₗ[ℝ] Dual E 𝕜`, and, in the context of normed spaces `StrongDual.extendRCLikeₗᵢ : StrongDual E ℝ ≃ₗᵢ[ℝ] StrongDual E 𝕜`.
Maldooor
pushed a commit
to Maldooor/mathlib4
that referenced
this pull request
Feb 25, 2026
…ity#34530) This removes some `erw`s in the proof of the Hahn-Banach theorem by using `ContinuousLinearMap.extendTo𝕜'` instead of the unprimed version. While the diff adds a type ascription to the `hextends` argument in an `obtain`, so that it elaborates as `∀ x : p, g ↑x = fr x` instead of `∀ x : p.restrictScalars ℝ, g ↑x = fr x`, this is in fact helping to *avoid* defeq abuse (since the domain of `fr` is `↥p` not `↥(p.restrictScalars ℝ)`).
pfaffelh
pushed a commit
to pfaffelh/mathlib4
that referenced
this pull request
Mar 2, 2026
…nprover-community#34543) This PR concerns the extension of `ℝ`-linear (continuous or not) functionals to `𝕜`-linear functionals. This does several things, but I felt it was better to do it all at once, rather than having repeated churn in the same files because the current setup is a mess for numerous reasons. Unfortunately, that means the diff is a bit of a mess; I think the easiest way to review this PR is read the following discussion and then only look at the *new* code (and check that the deprecations exist). I will begin by highlighting the current problems: 1. Naming: the primary declarations `LinearMap.extendTo𝕜'` and `ContinuousLinearMap.extendTo𝕜'` are in the wrong namespaces (`Module.Dual` and `StrongDual`), and contain a variable name `𝕜`. 2. These declarations are primed, and their unprimed counterparts operate directly on `RestrictScalars`. This is nominally (according to the module documentation) for convenience, but it leads to defeq abuse (see leanprover-community#34530) and so should be avoided anyway. That PR removes the only occurrence of the use of the unprimed declarations in Mathlib. 3. The declaration `ContinuousLinearMap.extendTo𝕜'` has type class assumptions (normed ones) that are too strong, thereby making it unusable for non-normed spaces (e.g., when one wants to consider continuous linear functionals on the weak dual of a Banach space). 4. Point (3) led to the creation of `RCLike.extendTo𝕜'ₗ` which is just `ContinuousLinearMap.extendTo𝕜'` except reproven with weaker type class assumptions and bundled into a linear map. 5. There are missing `simp` lemmas, namely, ones concerning the imaginary part of the extension applied to a vector. 6. We're missing appropriately bundled versions, with `RCLike.extendTo𝕜'ₗ` being the only bundling currently. In this PR: we fix the above by doing the following: 1. Renaming `LinearMap.extendTo𝕜'` → `Module.Dual.extendRCLike` and `ContinuousLinearMap.extendTo𝕜'` → `StrongDual.extendRCLike`. 2. Removing the unprimed counterparts that operate on `RestrictScalars` 3. Weakening the type class assumptions on the newly renamed `StrongDual.extendRCLike` 4. Move `RCLike.extendTo𝕜'ₗ` out of its current location (`Analysis/LocallyConvex/Separation`) and next to `StrongDual.extendRCLike`; use the newly generalized `StrongDual.extendRCLike` to define it; rename it to `StrongDual.extendRCLikeₗ`; upgrade it from a linear map to a linear equivalence. 5. Add the missing simp lemmas for imaginary parts. 6. Add other appropriate bundlings, namely `Module.Dual.extendRCLikeₗ : Dual E ℝ ≃ₗ[ℝ] Dual E 𝕜`, and, in the context of normed spaces `StrongDual.extendRCLikeₗᵢ : StrongDual E ℝ ≃ₗᵢ[ℝ] StrongDual E 𝕜`.
pevogam
pushed a commit
to pevogam/mathlib4
that referenced
this pull request
Mar 19, 2026
…nprover-community#34543) This PR concerns the extension of `ℝ`-linear (continuous or not) functionals to `𝕜`-linear functionals. This does several things, but I felt it was better to do it all at once, rather than having repeated churn in the same files because the current setup is a mess for numerous reasons. Unfortunately, that means the diff is a bit of a mess; I think the easiest way to review this PR is read the following discussion and then only look at the *new* code (and check that the deprecations exist). I will begin by highlighting the current problems: 1. Naming: the primary declarations `LinearMap.extendTo𝕜'` and `ContinuousLinearMap.extendTo𝕜'` are in the wrong namespaces (`Module.Dual` and `StrongDual`), and contain a variable name `𝕜`. 2. These declarations are primed, and their unprimed counterparts operate directly on `RestrictScalars`. This is nominally (according to the module documentation) for convenience, but it leads to defeq abuse (see leanprover-community#34530) and so should be avoided anyway. That PR removes the only occurrence of the use of the unprimed declarations in Mathlib. 3. The declaration `ContinuousLinearMap.extendTo𝕜'` has type class assumptions (normed ones) that are too strong, thereby making it unusable for non-normed spaces (e.g., when one wants to consider continuous linear functionals on the weak dual of a Banach space). 4. Point (3) led to the creation of `RCLike.extendTo𝕜'ₗ` which is just `ContinuousLinearMap.extendTo𝕜'` except reproven with weaker type class assumptions and bundled into a linear map. 5. There are missing `simp` lemmas, namely, ones concerning the imaginary part of the extension applied to a vector. 6. We're missing appropriately bundled versions, with `RCLike.extendTo𝕜'ₗ` being the only bundling currently. In this PR: we fix the above by doing the following: 1. Renaming `LinearMap.extendTo𝕜'` → `Module.Dual.extendRCLike` and `ContinuousLinearMap.extendTo𝕜'` → `StrongDual.extendRCLike`. 2. Removing the unprimed counterparts that operate on `RestrictScalars` 3. Weakening the type class assumptions on the newly renamed `StrongDual.extendRCLike` 4. Move `RCLike.extendTo𝕜'ₗ` out of its current location (`Analysis/LocallyConvex/Separation`) and next to `StrongDual.extendRCLike`; use the newly generalized `StrongDual.extendRCLike` to define it; rename it to `StrongDual.extendRCLikeₗ`; upgrade it from a linear map to a linear equivalence. 5. Add the missing simp lemmas for imaginary parts. 6. Add other appropriate bundlings, namely `Module.Dual.extendRCLikeₗ : Dual E ℝ ≃ₗ[ℝ] Dual E 𝕜`, and, in the context of normed spaces `StrongDual.extendRCLikeₗᵢ : StrongDual E ℝ ≃ₗᵢ[ℝ] StrongDual E 𝕜`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This removes some
erws in the proof of the Hahn-Banach theorem by usingContinuousLinearMap.extendTo𝕜'instead of the unprimed version.While the diff adds a type ascription to the
hextendsargument in anobtain, so that it elaborates as∀ x : p, g ↑x = fr xinstead of∀ x : p.restrictScalars ℝ, g ↑x = fr x, this is in fact helping to avoid defeq abuse (since the domain offris↥pnot↥(p.restrictScalars ℝ)).