Commit 2022-12-14 23:20 d37e4a64

View on Github →

feat port: Data.Int.CharZero (#1029) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/CharZero.lean

added theorem Int.cast_div_charZero

added theorem Int.cast_eq_zero

added theorem Int.cast_inj

added theorem Int.cast_injective

added theorem Int.cast_ne_zero

added theorem RingHom.injective_int