mathlib3
refactor(ring_theory/algebra): alg_hom extends ring_hom and use curly brackets
#1529

Merged

refactor(ring_theory/algebra): alg_hom extends ring_hom and use curly brackets #1529

mergify merged 6 commits into master from alg_hom

chore(algebra/ring): use curly brackets for ring_hom where possible

e1687581

refactor(ring_theory/algebra): alg_hom extends ring_hom and use curly…

4532d248

fix build

695e7185

ChrisHughes24 added blocked-by-other-PR

jcommelin commented on 2019-10-09

Update src/ring_theory/algebra.lean

88a1944d

ChrisHughes24 added awaiting-review

ChrisHughes24 removed blocked-by-other-PR

Merge branch 'master' into alg_hom

6b211f51

fix build

bfc6bcd5

jcommelin approved these changes on 2019-10-11

jcommelin added ready-to-merge

mergify merged d5de8037 into master 6 years ago

mergify deleted the alg_hom branch 6 years ago

YaelDillies removed awaiting-review

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone