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

Commit
6 years ago
chore(algebra/ring): use curly brackets for ring_hom where possible (#1525) * chore(algebra/ring): use curly brackets for ring_hom where possible * add comments explaining motivation * move explanation to header * fix build * Update src/algebra/ring.lean * scott's suggestion
Author
Committer
Parents
Loading