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
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