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: port Analysis.Normed.Ring.Seminorm #3211

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: port Analysis.Normed.Ring.Seminorm #3211

wants to merge 13 commits into from

Conversation

AlexKontorovich
Copy link
Collaborator

@AlexKontorovich AlexKontorovich commented Mar 31, 2023 •
edited by hrmacbeth
Loading

This is currently stuck on an issue as indicated in line 111. edit: fixed by the etaExperiment option

Open in Gitpod

@AlexKontorovich
feat: port Analysis.Normed.Ring.Seminorm
85385f2
@AlexKontorovich
Initial file copy from mathport
99557a2
@AlexKontorovich
automated fixes
9b95e05 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@AlexKontorovich
some bugs identified
4fcf2cf
@AlexKontorovich AlexKontorovich added the help-wanted The author needs attention to resolve issues label Mar 31, 2023
@hrmacbeth hrmacbeth removed the help-wanted The author needs attention to resolve issues label Mar 31, 2023
@AlexKontorovich AlexKontorovich added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Apr 3, 2023
@AlexKontorovich AlexKontorovich added help-wanted The author needs attention to resolve issues and removed awaiting-review labels Apr 3, 2023
@AlexKontorovich
Copy link
Collaborator Author

Lint is complaining about some simp lemmas about toFun not being in simp normal form. But when I change that, it's complaining that the lemma is a tautology. So what's the right formulation here? Thanks!

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 11, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 16, 2023
@int-y1
Copy link
Collaborator

int-y1 commented Apr 16, 2023

Lint is complaining about some simp lemmas about toFun not being in simp normal form. But when I change that, it's complaining that the lemma is a tautology. So what's the right formulation here? Thanks!

I saw 4 lint errors for 4 different theorems. You may have confused them.

RingSeminorm.toFun_eq_coe
MulRingSeminorm.toFun_eq_coe
RingNorm.toFun_eq_coe
MulRingNorm.toFun_eq_coe

@int-y1 int-y1 added awaiting-review and removed help-wanted The author needs attention to resolve issues labels Apr 16, 2023
@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 17, 2023
bors bot pushed a commit that referenced this pull request Apr 17, 2023
@AlexKontorovich @hrmacbeth
@int-y1 @Parcly-Taxel
feat: port Analysis.Normed.Ring.Seminorm (#3211)
2313f45 
~~This is currently stuck on an issue as indicated in line 111.~~ edit: fixed by the `etaExperiment` option



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
@bors
Copy link

bors bot commented Apr 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Analysis.Normed.Ring.Seminorm [Merged by Bors] - feat: port Analysis.Normed.Ring.Seminorm Apr 17, 2023
@bors bors bot closed this Apr 17, 2023
@bors bors bot deleted the port/Analysis.Normed.Ring.Seminorm branch April 17, 2023 09:04
semorrison pushed a commit that referenced this pull request May 10, 2023
@AlexKontorovich @hrmacbeth
@int-y1 @Parcly-Taxel
feat: port Analysis.Normed.Ring.Seminorm (#3211)
60222a7 
~~This is currently stuck on an issue as indicated in line 111.~~ edit: fixed by the `etaExperiment` option



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@AlexKontorovich @int-y1 @semorrison @hrmacbeth @Parcly-Taxel