Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-16 17:03 acee671f

View on Github →

chore(data/{nat,int}/cast/field): generalize to division_ring (#18598) Notably, this now works on quaternions. Forward-ported at https://github.com/leanprover-community/mathlib4/pull/2928

Estimated changes

Modified src/algebra/char_zero/lemmas.lean

modified theorem nat.cast_div_char_zero

Modified src/data/int/cast/field.lean

modified theorem int.cast_div

modified theorem int.cast_neg_nat_cast

Modified src/data/int/char_zero.lean

modified theorem int.cast_div_char_zero

Modified src/data/nat/cast/field.lean

modified theorem nat.cast_div

modified theorem nat.cast_div_div_div_cancel_right