mathlib3
chore(algebra/ring): use curly brackets for ring_hom where possible
#1525
Merged
Overview
Commits
7
Changes
View On GitHub

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

mergify merged 7 commits into master from ring_hom_brackets
ChrisHughes24
ChrisHughes24 chore(algebra/ring): use curly brackets for ring_hom where possible
e1687581
rwbarton
ChrisHughes24 add comments explaining motivation
fdc34b17
ChrisHughes24 move explanation to header
878b9fc8
ChrisHughes24 fix build
c152f3a0
ChrisHughes24 ChrisHughes24 added awaiting-review
kim-em
kim-em commented on 2019-10-11
kim-em Update src/algebra/ring.lean
00f28c41
kim-em
kim-em commented on 2019-10-11
ChrisHughes24 scott's suggestion
fac193f7
jcommelin
jcommelin approved these changes on 2019-10-11
jcommelin jcommelin removed awaiting-review
jcommelin jcommelin added ready-to-merge
mergify[bot] Merge branch 'master' into ring_hom_brackets
70bb40c6
mergify mergify merged 6b7377aa into master 6 years ago
mergify mergify deleted the ring_hom_brackets branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum