Commit 2022-12-14 15:48 61138ea1

View on Github →

feat port: Data.Int.Cast.Field (#1016) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Cast/Field.lean

added theorem Int.cast_div

added theorem Int.cast_neg_natCast