Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-19 11:58 7ddaf104

View on Github →

chore(algebra/algebra): algebra_map_int_eq (#11474) from flt-regular

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem algebra_map_int_eq

Modified src/data/polynomial/algebra_map.lean

deleted theorem polynomial.eval₂_algebra_map_int_X

added theorem polynomial.eval₂_int_cast_ring_hom_X

deleted theorem polynomial.ring_hom_eval₂_algebra_map_int

added theorem polynomial.ring_hom_eval₂_cast_int_ring_hom