Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem #12787

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem #12787

wants to merge 25 commits into from

Conversation

j-loreaux
Copy link
Collaborator

@j-loreaux j-loreaux commented Mar 17, 2022 •
edited by github-actions bot

Gelfand-Mazur theorem For a complex Banach division algebra, the natural algebra_map ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a.

Open in Gitpod

j-loreaux and others added 21 commits February 18, 2022 13:47
@j-loreaux
add normed division ring
fa6191a
@j-loreaux
remove the normed_group instance
3d18572
@j-loreaux
delete normed_field lemmas
0f35c06 
This does several things:
1. Moves the division ring lemmas into root namespace
2. Deletes the corresponding lemmas from the normed field namespace
3. Deletes the `normed_field.` references across mathlib
@j-loreaux
add list.norm_prod and list.nnnorm_prod
17f855c
@j-loreaux
rename instances
4868df6
@j-loreaux
fix a stray deletion of normed_field. which was needed.
521078a
@j-loreaux
merge master
fe8fca4
@j-loreaux
fix analysis.normed_space.basic
76792b6
@j-loreaux
remove extraneous normed_field. deletions
5172ca2
@j-loreaux
remove stray x
04aecc7
@j-loreaux
simplify proof of list.norm_prod with norm_hom (and nnnorm)
242939d
@j-loreaux
generalize has_continuous_inv0 to normed division ring
94b0b05
@j-loreaux
workaround ac_refl
61384f7
@j-loreaux
Merge branch 'master' into j-loreaux/normed-division-ring
da41d26
@eric-wieser
Merge remote-tracking branch 'origin/master' into j-loreaux/normed-di…
1c0ab91 
…vision-ring

Conflicts resolved with `git diff $(git merge-base HEAD^ origin/master)..HEAD^ -- src/analysis/normed_space/basic.lean | patch src/analysis/normed/normed_field.lean`
@j-loreaux
apply suggestions from code review
eb9937e
@j-loreaux
protect list.norm_prod
c13e111
@j-loreaux
Merge branch 'master' into j-loreaux/normed-division-ring
fc188b3
@j-loreaux
make quaternions a normed_division_ring
a6fd68b
@j-loreaux
use mul_mul_mul_comm
fc784a6
@j-loreaux
Provide the Gelfand-Mazur isomorphism
49fd807
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Mar 17, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 17, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Mar 17, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 18, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@eric-wieser
Copy link
Member

Can you merge master to make the diff shrink?

@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 18, 2022
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 18, 2022
@dupuisf
Copy link
Collaborator

dupuisf commented Mar 19, 2022

Looks good!

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 19, 2022
bors bot pushed a commit that referenced this pull request Mar 19, 2022
@j-loreaux @eric-wieser
feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem (…
6abfb1d 
…#12787)

**Gelfand-Mazur theorem** For a complex Banach division algebra, the natural `algebra_map ℂ A` is an algebra isomorphism whose inverse is given by selecting the (unique) element of `spectrum ℂ a`.

- [x] depends on: #12132 



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Mar 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem [Merged by Bors] - feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem Mar 20, 2022
@bors bors bot closed this Mar 20, 2022
@bors bors bot deleted the j-loreaux/gelfand-mazur' branch March 20, 2022 00:06
jjaassoonn pushed a commit that referenced this pull request Mar 20, 2022
@j-loreaux @eric-wieser @jjaassoonn
feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem (…
2fe40df 
…#12787)

**Gelfand-Mazur theorem** For a complex Banach division algebra, the natural `algebra_map ℂ A` is an algebra isomorphism whose inverse is given by selecting the (unique) element of `spectrum ℂ a`.

- [x] depends on: #12132 



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jjaassoonn pushed a commit that referenced this pull request Mar 21, 2022
@j-loreaux @eric-wieser @jjaassoonn
feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem (…
2c04841 
…#12787)

**Gelfand-Mazur theorem** For a complex Banach division algebra, the natural `algebra_map ℂ A` is an algebra isomorphism whose inverse is given by selecting the (unique) element of `spectrum ℂ a`.

- [x] depends on: #12132 



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@j-loreaux @leanprover-community-bot-assistant @eric-wieser @dupuisf