Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-22 08:40 6a5a2b13

View on Github →

feat(data/rat/cast): drop an unneeded typeclass assumption (#15972)

  • drop [char_zero _] assumption in map_rat_cast;
  • golf ring_hom.eq_rat_cast, generalize to ring_hom_class.

Estimated changes

modified theorem star_rat_cast
added theorem eq_rat_cast
modified theorem map_rat_cast
deleted theorem ring_hom.eq_rat_cast
modified theorem is_algebraic_rat