mathlib3
feat(ring_theory/adjoin): adjoining elements to form subalgebras
#756
Merged

feat(ring_theory/adjoin): adjoining elements to form subalgebras #756

mergify merged 10 commits into master from algebra-adjoin
kckennylau
kckennylau feat(ring_theory/adjoin): adjoining elements to form subalgebras
9afe334d
cipher1024 cipher1024 assigned ChrisHughes24 ChrisHughes24 6 years ago
jcommelin
jcommelin commented on 2019-03-12
jcommelin
ChrisHughes24 Merge branch 'master' into algebra-adjoin
5e881610
jcommelin Merge branch 'master' into algebra-adjoin
b1998c7a
jcommelin Merge branch 'master' into algebra-adjoin
f197b8a9
jcommelin
jcommelin commented on 2019-04-13
jcommelin Merge branch 'master' into algebra-adjoin
d794cde4
jcommelin jcommelin requested a review 6 years ago
jcommelin Fix build
140cbff4
jcommelin Change to_submodule into a coercion
97e7f3f4
jcommelin Use pointwise_mul
decc7de8
jcommelin jcommelin added ready-to-merge
ChrisHughes24
ChrisHughes24 dismissed these changes on 2019-03-12
jcommelin jcommelin removed ready-to-merge
ChrisHughes24 add simp attribute to adjoin_empty
f4a6f69c
mergify mergify dismissed their stale review 6 years ago
Pull request has been modified.
ChrisHughes24
ChrisHughes24 approved these changes on 2019-05-05
ChrisHughes24 ChrisHughes24 added ready-to-merge
ChrisHughes24 Merge branch 'master' into algebra-adjoin
52d90166
ChrisHughes24
ChrisHughes24 dismissed these changes on 2019-05-05
mergify mergify dismissed their stale review 6 years ago
Pull request has been modified.
ChrisHughes24
ChrisHughes24 approved these changes on 2019-05-05
mergify mergify merged 23270e71 into master 6 years ago
mergify mergify deleted the algebra-adjoin branch 6 years ago

Login to write a write a comment.

Login via GitHub

Assignees
Labels
Milestone