Commit 2023-03-17 09:39 30413fc8
View on Github →chore(algebra): generalize typeclass arguments from field to semifield (#18597)
This generalizes some typeclass arguments from field
to semifield
and division_ring
to division_semiring
.
The proof for map_inv_nat_cast_smul
had to be rewritten, as it was previously proved in terms of map_inv_int_cast_smul
.
The latter is now instead proved in terms of the former.
Forward-ported in https://github.com/leanprover-community/mathlib4/pull/2926