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.

Sign up for GitHub

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/basic): add normed_division_ring #12132

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/basic): add normed_division_ring #12132

wants to merge 20 commits into from

Conversation

j-loreaux
Copy link
Collaborator

@j-loreaux j-loreaux commented Feb 18, 2022 •
edited by eric-wieser

This defines normed division rings and generalizes some of the lemmas that applied to normed fields instead to normed division rings.

This breaks one ac_refl; although this could be resolved by using simp only {canonize_instances := tt} first, it's easier to just tweak the proof.

Open in Gitpod

@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 Feb 18, 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 Feb 18, 2022
@j-loreaux j-loreaux 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 Feb 19, 2022
@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 j-loreaux mentioned this pull request Feb 20, 2022
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Feb 21, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 21, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 21, 2022
@eric-wieser
Copy link
Member

The failure looks like a bug in ac_refl, but mul_mul_mul_comm can close the goal anyway

@j-loreaux j-loreaux removed the awaiting-author A reviewer has asked the author a question or requested changes label Feb 22, 2022
@eric-wieser
Copy link
Member

I thought I'd use it as an exercise in teaching myself how to deal with this sort of merge in git via git diff ... | patch ...

YaelDillies
YaelDillies reviewed Mar 10, 2022
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Minor things

src/analysis/normed/normed_field.lean Outdated Show resolved Hide resolved
src/analysis/normed/normed_field.lean Outdated Show resolved Hide resolved
src/analysis/normed/normed_field.lean Outdated Show resolved Hide resolved
src/analysis/normed/normed_field.lean Show resolved Hide resolved
src/analysis/normed/normed_field.lean Outdated Show resolved Hide resolved
@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
@eric-wieser
Copy link
Member

eric-wieser commented Mar 17, 2022 •
edited

Can you add a quaternion.normed_division_ring instance just after instead of the existing quaternion.normed_ring one?

@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 17, 2022
@j-loreaux
Copy link
Collaborator Author

I replaced the quaternion.normed_ring instance with quaternion.normed_division_ring

@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 17, 2022
eric-wieser
eric-wieser approved these changes Mar 17, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

Let's hope CI doesn't fail mysteriously this time

@bors
Copy link

bors bot commented Mar 17, 2022

✌️ 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.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Mar 17, 2022
@j-loreaux
Copy link
Collaborator Author

bors r+

@j-loreaux j-loreaux mentioned this pull request Mar 17, 2022
Closed
1 task
bors bot pushed a commit that referenced this pull request Mar 17, 2022
@j-loreaux @eric-wieser
feat(analysis/normed_space/basic): add normed_division_ring (#12132)
a26dfc4 
This defines normed division rings and generalizes some of the lemmas that applied to normed fields instead to normed division rings.

This breaks one `ac_refl`; although this could be resolved by using `simp only {canonize_instances := tt}` first, it's easier to just tweak the proof.



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

bors bot commented Mar 18, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/normed_space/basic): add normed_division_ring [Merged by Bors] - feat(analysis/normed_space/basic): add normed_division_ring Mar 18, 2022
@bors bors bot closed this Mar 18, 2022
@bors bors bot deleted the j-loreaux/normed-division-ring branch March 18, 2022 00:28
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>
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/basic): add normed_division_ring (#12132)
2094349 
This defines normed division rings and generalizes some of the lemmas that applied to normed fields instead to normed division rings.

This breaks one `ac_refl`; although this could be resolved by using `simp only {canonize_instances := tt}` first, it's easier to just tweak the proof.



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

@YaelDillies YaelDillies YaelDillies left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
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 @YaelDillies