Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-29 08:18 3e2fb4c7

View on Github →

feat(data/rat/cast): generalize ext lemmas (#16268)

  • generalize monoid_with_zero_hom.ext_rat to monoid_with_zero;
  • deduce ext lemma for ring_homs from monoid_with_zero_hom version;
  • use hom classes.

Estimated changes

modified theorem ring_hom.ext_rat