Skip to content

[Merged by Bors] - feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemmas#16266

Closed
j-loreaux wants to merge 8 commits intomasterfrom
j-loreaux/CStarRing.norm_le_iff
Closed

[Merged by Bors] - feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemmas#16266
j-loreaux wants to merge 8 commits intomasterfrom
j-loreaux/CStarRing.norm_le_iff

Conversation

@j-loreaux
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux commented Aug 29, 2024

Open in Gitpod

@j-loreaux j-loreaux requested a review from dupuisf August 29, 2024 16:16
@j-loreaux j-loreaux added the t-analysis Analysis (normed *, calculus) label Aug 29, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 29, 2024 •
edited
Loading

PR summary 483ef8dcc9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ CFC.exists_pos_algebraMap_le_iff
+ CFC.le_one
+ CFC.le_one_iff
+ CFC.one_le
+ CFC.one_le_iff
+ _root_.ContinuousOn.ofReal_map_toNNReal
+ algebraMap_le_cfc_iff
+ algebraMap_le_iff_le_spectrum
+ cfc_le_algebraMap_iff
+ cfc_le_one_iff
+ cfc_nnreal_le_iff
+ conjugate_le_norm_smul
+ conjugate_le_norm_smul'
+ instNonnegSpectrumClassComplexNonUnital
+ le_algebraMap_iff_spectrum_le
+ nnnorm_le_iff_of_nonneg
+ nnnorm_le_natCast_iff_of_nonneg
+ nnnorm_le_one_iff_of_nonneg
+ nnnorm_mem_spectrum_of_nonneg
+ norm_le_iff_le_algebraMap
+ norm_le_natCast_iff_of_nonneg
+ norm_le_norm_of_nonneg_of_le
+ norm_le_one_iff_of_nonneg
+ norm_mem_spectrum_of_nonneg
+ norm_or_neg_norm_mem_spectrum
+ one_le_cfc_iff
- CStarRing.conjugate_le_norm_smul
- CStarRing.conjugate_le_norm_smul'
- CStarRing.instNonnegSpectrumClassComplexNonUnital
- CStarRing.nnnorm_mem_spectrum_of_nonneg
- CStarRing.norm_le_norm_of_nonneg_of_le
- CStarRing.norm_mem_spectrum_of_nonneg
- CStarRing.norm_or_neg_norm_mem_spectrum

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 script/declarations_diff.sh contains some details about this script.

dupuisf
dupuisf reviewed Aug 29, 2024
View reviewed changes
@dupuisf dupuisf added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 29, 2024
j-loreaux and others added 3 commits August 30, 2024 16:29
@j-loreaux @dupuisf
code review
d12bf84 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
@j-loreaux
fix
84cf62c
@j-loreaux
rename
d6eb4c8
@j-loreaux j-loreaux removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 30, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Aug 30, 2024 •
edited
Loading

@dupuisf just so you're aware, I not only fixed the lemma names, but I also added a few new lemmas too.

I'm open to putting ContinuousOn.ofReal_map_toReal elsewhere if you want, but it is pretty specialized.

dupuisf
dupuisf reviewed Aug 31, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@dupuisf dupuisf left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few last comments, but otherwise LGTM.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 31, 2024
@j-loreaux j-loreaux mentioned this pull request Aug 31, 2024
Closed
7 tasks
@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Aug 31, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 31, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 31, 2024
@j-loreaux
feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemm…
a2abea1 
…as (#16266)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemmas [Merged by Bors] - feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemmas Aug 31, 2024
@mathlib-bors mathlib-bors bot closed this Aug 31, 2024
@mathlib-bors mathlib-bors bot deleted the j-loreaux/CStarRing.norm_le_iff branch August 31, 2024 15:57
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@j-loreaux @bjoernkjoshanssen
feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemm…
a626ebe 
…as (#16266)
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@j-loreaux @bjoernkjoshanssen
feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemm…
854d740 
…as (#16266)
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@j-loreaux @bjoernkjoshanssen
feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemm…
94a46f8 
…as (#16266)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf dupuisf left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@j-loreaux @dupuisf