Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-28 20:07 a148d797

View on Github →

chore(*): revert #17048 (#17733) This had merge conflicts which I've been rather reckless about resolving. Let's see what CI says.

Estimated changes

modified theorem int.cast_pow
modified theorem int.coe_nat_pow
modified theorem nat.cast_pow
deleted theorem coe_div₀
deleted theorem coe_inv₀
deleted theorem coe_bit0
deleted theorem coe_bit1
deleted theorem coe_div
deleted theorem coe_inv
deleted theorem coe_pow
deleted theorem coe_zpow
added theorem add_monoid_hom.coe_mul
deleted def coe_is_linear_map
deleted theorem coe_smulₛₗ
added theorem linear_map.coe_mul
added theorem linear_map.coe_one
added theorem submodule.coe_add
added theorem submodule.coe_smul
added theorem submodule.coe_zero
added theorem dfinsupp.coe_add
added theorem dfinsupp.coe_neg
added theorem dfinsupp.coe_nsmul
added theorem dfinsupp.coe_smul
added theorem dfinsupp.coe_sub
added theorem dfinsupp.coe_zero
added theorem dfinsupp.coe_zsmul
added theorem enat.coe_add
added theorem enat.coe_mul
added theorem enat.coe_one
added theorem enat.coe_sub
added theorem enat.coe_zero
added theorem finset.coe_one
added theorem finsupp.coe_smul
added theorem finsupp.coe_add
added theorem finsupp.coe_neg
added theorem finsupp.coe_sub
added theorem finsupp.coe_zero
added theorem finsupp.coe_mul
modified theorem int.cast_add
modified theorem int.cast_bit0
modified theorem int.cast_bit1
modified theorem int.cast_four
modified theorem int.cast_neg
modified theorem int.cast_one
modified theorem int.cast_sub
modified theorem int.cast_three
modified theorem int.cast_two
modified theorem int.cast_zero
modified def int.cast_add_hom
modified theorem int.cast_mul
modified theorem nat.cast_add
modified theorem nat.cast_bit0
modified theorem nat.cast_bit1
modified theorem nat.cast_one
modified theorem nat.cast_zero
modified theorem rat.cast_add
modified theorem rat.cast_bit0
modified theorem rat.cast_bit1
modified theorem rat.cast_div
modified def rat.cast_hom
modified theorem rat.cast_inv
modified theorem rat.cast_mul
modified theorem rat.cast_pow
modified theorem rat.cast_sub
modified theorem rat.cast_zpow
added theorem nnrat.coe_add
added theorem nnrat.coe_bit0
added theorem nnrat.coe_bit1
added theorem nnrat.coe_div
added theorem nnrat.coe_inv
added theorem nnrat.coe_mul
added theorem nnrat.coe_one
added theorem nnrat.coe_sub
added theorem nnrat.coe_zero
added theorem ennreal.coe_add
added theorem ennreal.coe_bit0
added theorem ennreal.coe_bit1
added theorem ennreal.coe_div
added theorem ennreal.coe_inv
added theorem ennreal.coe_mul
added theorem ennreal.coe_one
added theorem ennreal.coe_pow
added theorem ennreal.coe_zero
modified theorem ennreal.zero_lt_two
added theorem ereal.coe_add
added theorem ereal.coe_bit0
added theorem ereal.coe_bit1
added theorem ereal.coe_mul
added theorem ereal.coe_nsmul
added theorem ereal.coe_one
added theorem ereal.coe_pow
added theorem ereal.coe_zero
added theorem equiv.perm.coe_mul
added theorem equiv.perm.coe_one
modified theorem subgroup.coe_pow
modified theorem subgroup.coe_zpow
modified theorem subgroup_class.coe_zpow
added theorem one_mem_class.coe_one
added theorem submonoid.coe_mul
added theorem submonoid.coe_one
modified theorem submonoid.coe_pow
modified theorem submonoid_class.coe_pow
added theorem mul_mem_class.coe_mul
added theorem lucas_lehmer.X.coe_mul
added theorem polynomial.coe_add
added theorem polynomial.coe_bit0
added theorem polynomial.coe_bit1
added theorem polynomial.coe_mul
added theorem polynomial.coe_one
added theorem polynomial.coe_pow
added theorem polynomial.coe_zero
modified theorem subring.coe_pow
modified def subring_class.subtype
modified theorem subsemiring.coe_pow
modified theorem subsemiring_class.coe_pow
modified theorem cardinal.nat_cast_pow
added theorem continuous_map.coe_div
added theorem continuous_map.coe_inv
added theorem continuous_map.coe_mul
added theorem continuous_map.coe_one
added theorem continuous_map.coe_pow
added theorem add_circle.coe_neg
added theorem add_circle.coe_nsmul
added theorem add_circle.coe_zsmul