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 src/algebra/module/basic.lean

modified theorem inv_nat_cast_smul_comm

modified theorem inv_nat_cast_smul_eq

modified theorem map_inv_nat_cast_smul

Modified src/algebra/periodic.lean

modified theorem function.antiperiodic.const_inv_mul

modified theorem function.antiperiodic.const_inv_smul₀

modified theorem function.antiperiodic.const_mul

modified theorem function.antiperiodic.const_smul₀

modified theorem function.antiperiodic.mul_const'

modified theorem function.antiperiodic.mul_const

modified theorem function.antiperiodic.mul_const_inv

modified theorem function.periodic.const_inv_mul

modified theorem function.periodic.const_inv_smul₀

modified theorem function.periodic.const_smul₀

modified theorem function.periodic.div_const

modified theorem function.periodic.mul_const'

modified theorem function.periodic.mul_const

modified theorem function.periodic.mul_const_inv

Modified src/algebra/star/basic.lean

modified theorem star_div'

modified theorem star_inv'

modified theorem star_zpow₀

Modified src/algebra/star/module.lean

modified theorem star_inv_nat_cast_smul

Modified src/algebra/star/pointwise.lean

Modified src/algebra/star/self_adjoint.lean

Modified src/data/matrix/basic.lean

modified theorem matrix.conj_transpose_inv_nat_cast_smul