Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(topology/algebra/group): • lemmas#17383

Closed
YaelDillies wants to merge 5 commits intomasterfrom
is_open_smul
Closed

[Merged by Bors] - feat(topology/algebra/group): • lemmas#17383
YaelDillies wants to merge 5 commits intomasterfrom
is_open_smul

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies commented Nov 6, 2022

Write the smul version of several mul lemmas, along with the missing instance has_continuous_mul M M → has_continuous_smul Mᵐᵒᵖ M

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) t-topology Topological spaces, uniform spaces, metric spaces, filters labels Nov 6, 2022
@YaelDillies YaelDillies requested a review from urkud November 6, 2022 11:45
@YaelDillies YaelDillies mentioned this pull request Nov 6, 2022
Closed
2 tasks
eric-wieser
eric-wieser reviewed Nov 6, 2022
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 6, 2022
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 6, 2022
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 6, 2022
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 6, 2022
View reviewed changes
eric-wieser
eric-wieser approved these changes Nov 6, 2022
View reviewed changes
Copy link
Copy Markdown
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.

bors d+

Thanks!

@bors
Copy link
Copy Markdown

bors bot commented Nov 6, 2022

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

@eric-wieser eric-wieser added the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 6, 2022
@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 Nov 6, 2022
@YaelDillies YaelDillies removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 7, 2022
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Nov 7, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 7, 2022
@YaelDillies
feat(topology/algebra/group): • lemmas (#17383)
1f19543 
Write the `smul` version of several `mul` lemmas, along with the missing instance `has_continuous_mul M M → has_continuous_smul Mᵐᵒᵖ M`
@bors
Copy link
Copy Markdown

bors bot commented Nov 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/algebra/group): • lemmas [Merged by Bors] - feat(topology/algebra/group): • lemmas Nov 7, 2022
@bors bors bot closed this Nov 7, 2022
@bors bors bot deleted the is_open_smul branch November 7, 2022 13:00
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@urkud urkud Awaiting requested review from urkud

1 more reviewer

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

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. t-algebra Algebra (groups, rings, fields etc) t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @eric-wieser @leanprover-community-bot-assistant