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

[Merged by Bors] - feat(algebra/lie/nilpotent): add lemma lie_module.coe_lower_central_series_ideal_le #11851

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(algebra/lie/nilpotent): add lemma lie_module.coe_lower_central_series_ideal_le #11851

wants to merge 1 commit into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented Feb 5, 2022

Open in Gitpod

@ocfnash ocfnash added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Feb 5, 2022
jcommelin
jcommelin approved these changes Feb 5, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin 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 merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Feb 5, 2022
bors bot pushed a commit that referenced this pull request Feb 5, 2022
@ocfnash
feat(algebra/lie/nilpotent): add lemma `lie_module.coe_lower_central_…
9fcd1f2 
…series_ideal_le` (#11851)
@bors
Copy link

bors bot commented Feb 5, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/lie/nilpotent): add lemma lie_module.coe_lower_central_series_ideal_le [Merged by Bors] - feat(algebra/lie/nilpotent): add lemma lie_module.coe_lower_central_series_ideal_le Feb 5, 2022
@bors bors bot closed this Feb 5, 2022
@bors bors bot deleted the ocfnash/lie_nilp_1 branch February 5, 2022 18:28
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
easy < 20s of review time. See the lifecycle page for guidelines. 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.
3 participants
@ocfnash @jcommelin @leanprover-community-bot-assistant