Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

modified theorem star_div'
modified theorem star_inv'
modified theorem star_zpow₀