Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-11 13:15 6b7377aa

View on Github →

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

Estimated changes