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

[Merged by Bors] - feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) #12178

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) #12178

wants to merge 4 commits into from

Conversation

Vierkantor
Copy link
Collaborator

Two useful lemmas on the submodule spanned by I-scalar multiples.

Open in Gitpod

@Vierkantor Vierkantor 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 21, 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 21, 2022
@semorrison
Copy link
Collaborator

bors merge

@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 Feb 26, 2022
bors bot pushed a commit that referenced this pull request Feb 26, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
ae81044 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 26, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Feb 27, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
35aff61 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 27, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Feb 27, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
c6bb319 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 27, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Feb 27, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
114ac71 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 27, 2022

Build failed:

Vierkantor and others added 4 commits February 28, 2022 09:06
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M)
20f6d28 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.
@Vierkantor @eric-wieser
dedot
b4d4976 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@Vierkantor @eric-wieser
Add empty line
b3080b3 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@Vierkantor
Fix (smul_induction_on needs less parameters)
037bde6
@Vierkantor Vierkantor added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Feb 28, 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 28, 2022
Vierkantor added a commit that referenced this pull request Mar 2, 2022
@Vierkantor
feat(ring_theory/ideal): more lemmas on ideals multiplied with submod…
fa8c9d0 
…ules

These are, like #12178, split off from #12287
@Vierkantor Vierkantor mentioned this pull request Mar 2, 2022
Closed
@riccardobrasca
Copy link
Member

Thanks!

bors merge

@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 3, 2022
bors bot pushed a commit that referenced this pull request Mar 3, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
129cd8f 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Mar 3, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Mar 3, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
03ac316 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Mar 3, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Mar 3, 2022
@Vierkantor
feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) (#12178)
4dec7b5 
Two useful lemmas on the submodule spanned by `I`-scalar multiples.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors
Copy link

bors bot commented Mar 3, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) [Merged by Bors] - feat(ring_theory/ideal): (I : ideal R) • (⊤ : submodule R M) Mar 3, 2022
@bors bors bot closed this Mar 3, 2022
@bors bors bot deleted the ideal_smul_submodule_lemmas branch March 3, 2022 16:19
bors bot pushed a commit that referenced this pull request Mar 3, 2022
@Vierkantor
feat(ring_theory/ideal): more lemmas on ideals multiplied with submod…
9deac65 
…ules (#12401)

These are, like #12178, split off from #12287
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
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
@Vierkantor @semorrison @riccardobrasca @eric-wieser