Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-10 16:17 168ad7fc

View on Github →

feat(data/nat/cast): generalize to fun_like (#11128)

Estimated changes

Modified archive/100-theorems-list/16_abel_ruffini.lean

Modified src/algebra/algebra/basic.lean

deleted theorem alg_hom.map_nat_cast

Modified src/algebra/char_p/basic.lean

modified theorem frobenius_nat_cast

Modified src/algebra/char_p/pi.lean

Modified src/algebra/char_p/quotient.lean

Modified src/algebra/char_p/subring.lean

Modified src/algebra/char_zero.lean

Modified src/algebra/group_power/lemmas.lean

Modified src/algebra/ne_zero.lean

added theorem ne_zero.nat_of_injective

deleted theorem ne_zero.of_injective'

modified theorem ne_zero.of_injective

Modified src/data/complex/basic.lean

Modified src/data/complex/is_R_or_C.lean

Modified src/data/int/cast.lean

Modified src/data/matrix/char_p.lean

Modified src/data/nat/cast.lean

deleted theorem add_monoid_hom.eq_nat_cast

modified theorem add_monoid_hom.ext_nat

deleted theorem add_monoid_hom.map_nat_cast

added theorem eq_nat_cast'

added theorem eq_nat_cast

added theorem ext_nat''

added theorem ext_nat'

added theorem ext_nat

added theorem map_nat_cast'

added theorem map_nat_cast

modified theorem monoid_with_zero_hom.ext_nat

modified theorem nat.cast_one

modified theorem nat.cast_two

modified theorem nat.coe_nat_dvd

modified theorem nat.commute_cast

deleted theorem ring_hom.eq_nat_cast

deleted theorem ring_hom.ext_nat

deleted theorem ring_hom.map_nat_cast

modified theorem with_top.coe_nat

Modified src/data/polynomial/algebra_map.lean

Modified src/data/polynomial/basic.lean

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/eval.lean

deleted theorem polynomial.map_nat_cast

Modified src/data/real/nnreal.lean

Modified src/data/zmod/basic.lean

Modified src/number_theory/basic.lean

Modified src/number_theory/class_number/finite.lean

Modified src/number_theory/cyclotomic/basic.lean

Modified src/number_theory/padics/ring_homs.lean

Modified src/ring_theory/perfection.lean

Modified src/ring_theory/polynomial/basic.lean

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/dickson.lean

Modified src/ring_theory/polynomial/pochhammer.lean

Modified src/ring_theory/subring/basic.lean

modified theorem subring.coe_nat_cast

Modified src/ring_theory/witt_vector/compare.lean

Modified src/ring_theory/witt_vector/is_poly.lean

Modified src/ring_theory/witt_vector/verschiebung.lean

Modified src/ring_theory/witt_vector/witt_polynomial.lean