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

feat(ring_theory/derivation): support non-commutative rings (via bimodules)#18936

Open
eric-wieser wants to merge 4 commits intomasterfrom
eric-wieser/derivation-bimodule
Open

feat(ring_theory/derivation): support non-commutative rings (via bimodules)#18936
eric-wieser wants to merge 4 commits intomasterfrom
eric-wieser/derivation-bimodule

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented May 3, 2023

I expect this to be a non-starter without:

I figured I'd make the PR for future reference anyway.


Open in Gitpod

(feel free to port this file without waiting for this PR)

@eric-wieser eric-wieser added the WIP Work in progress label May 3, 2023
@eric-wieser eric-wieser changed the title Eric wieser/derivation bimodule feat(ring_theory/derivation): support non-commutative rings (via bimodules) May 3, 2023
@eric-wieser eric-wieser force-pushed the eric-wieser/derivation-bimodule branch from 72f9419 to 8fafd52 Compare May 4, 2023 00:22
@ghost ghost 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 May 4, 2023
@ghost
Copy link
Copy Markdown

ghost commented May 4, 2023

This PR/issue depends on:

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

too-late This PR was ready too late for inclusion in mathlib3 WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants