Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-27 21:20 533cbf45

View on Github →

feat(data/int/{cast, char_zero}): relax typeclass assumptions (#14413)

Estimated changes

Modified src/data/int/cast.lean

modified theorem int.cast_bit0

modified theorem int.cast_bit1

modified theorem int.cast_comm

modified theorem int.cast_commute

modified theorem int.cast_four

modified theorem int.cast_mul

modified def int.cast_ring_hom

modified theorem int.cast_three

modified theorem int.cast_two

modified theorem int.coe_cast_ring_hom

modified theorem int.commute_cast

modified theorem ring_hom.ext_int

Modified src/data/int/char_zero.lean

modified theorem ring_hom.injective_int