mathlib3
feat(ring_theory/derivation): The differential module under base change.
#17198

Open

feat(ring_theory/derivation): The differential module under base change. #17198

erdOne wants to merge 2 commits into master from kaehler_is_base_change

erdOne added awaiting-review

erdOne added blocked-by-other-PR

erdOne added t-algebra

mathlib-dependent-issues-bot removed blocked-by-other-PR

first commit

c8cdf2f3

erdOne force pushed from 58024535 to c8cdf2f3 3 years ago

jcommelin approved these changes on 2022-12-07

leanprover-community-bot-assistant added ready-to-merge

leanprover-community-bot-assistant removed awaiting-review

github-actions added delegated

Merge remote-tracking branch 'origin/master' into kaehler_is_base_change

cefbb99f

eric-wieser added awaiting-CI

kim-em added too-late

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge delegated awaiting-CI t-algebra too-late

Milestone

No milestone