[Merged by Bors] - refactor: Use StrongDual#28726
[Merged by Bors] - refactor: Use StrongDual#28726mans0954 wants to merge 63 commits intoleanprover-community:masterfrom
StrongDual#28726Conversation
PR summary 2c4da570e3Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 No changes to technical debt.You can run this locally as
|
|
There are a lot more occurrences: I could replace these if people think this is a useful thing to do? |
|
I'm certainly a fan of switching these. Are there any more to do? |
j-loreaux
added
the
awaiting-author
@j-loreaux I've done a search with which I think will have found everything. I deliberately haven't changed occurrences where doing so would distract from the symmetry - e.g. bilinear forms. I also steered away from I kept |
mans0954
removed
the
awaiting-author
j-loreaux
left a comment
j-loreaux
left a comment
There was a problem hiding this comment.
Please add this reasoning to the PR description in a form suitable for the git history:
I deliberately haven't changed occurrences where doing so would distract from the symmetry - e.g. bilinear forms. I also steered away from 𝕜 →L[𝕜] 𝕜 although I could change those to StrongDual 𝕜 𝕜 if you think that's better.
I kept E →L[𝕜] 𝕜 in Topology/Algebra/Module/WeakDual as WeakDual 𝕜 E := StrongDual 𝕜 E would look confusing!
And thanks for doing all this work!
bors d+
|
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
ghost
added
the
delegated
|
bors r+ |
The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in #27699. This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions: - Bilinear forms `M →L[R] E →L[R] R` and where using `StrongDual R M` would mask the symmetry of the statement; - The dual of rings / fields `R →L[R] R` and similar; - `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
StrongDualStrongDual
The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in leanprover-community#27699. This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions: - Bilinear forms `M →L[R] E →L[R] R` and where using `StrongDual R M` would mask the symmetry of the statement; - The dual of rings / fields `R →L[R] R` and similar; - `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.
The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in leanprover-community#27699. This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions: - Bilinear forms `M →L[R] E →L[R] R` and where using `StrongDual R M` would mask the symmetry of the statement; - The dual of rings / fields `R →L[R] R` and similar; - `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.
The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in leanprover-community#27699. This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions: - Bilinear forms `M →L[R] E →L[R] R` and where using `StrongDual R M` would mask the symmetry of the statement; - The dual of rings / fields `R →L[R] R` and similar; - `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.
2 participants
The
StrongDualabbrev forM →L[R] R, where the monoidMis a module over the semiringRandRandMare equipped with topologies, was introduced in #27699.This PR replaces existing occurrences of
M →L[R] RwithStrongDual R Metc. There are some exclusions:M →L[R] E →L[R] Rand where usingStrongDual R Mwould mask the symmetry of the statement;R →L[R] Rand similar;WeakDual 𝕜 MinTopology/Algebra/Module/WeakDual, where the focus is on the weak topology onM →L[R] R.