mathlib3
30413fc8 - chore(algebra): generalize typeclass arguments from field to semifield (#18597)

Commit
2 years ago
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 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading