Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-13 18:31 49f5fb88

View on Github →

chore(algebra/category/CommRing/limits): avoid is_ring_hom (#2142) define a ring_hom instead

Estimated changes