Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-27 23:52 e89510c2

View on Github →

fix(ring_theory/subsemiring/basic): make inclusion a ring_hom, not a monoid_hom (#13746)

Estimated changes

modified def subsemiring.inclusion