Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-09 09:48 d0532c10

View on Github →

feat(data/polynomial): lemmas about map (#530)

Estimated changes

Modified algebra/field.lean

added theorem is_field_hom.injective

Modified algebra/group.lean

added theorem is_group_hom.injective_iff

Modified data/polynomial.lean

added theorem polynomial.coeff_X

added theorem polynomial.degree_div_le

added theorem polynomial.degree_div_lt

added theorem polynomial.degree_map

deleted theorem polynomial.degree_map_eq

added theorem polynomial.degree_map_eq_of_injective

added theorem polynomial.degree_map_eq_of_leading_coeff_ne_zero

modified theorem polynomial.degree_mul_leading_coeff_inv

added theorem polynomial.div_mod_by_monic_unique

added theorem polynomial.div_zero

added theorem polynomial.eq_X_add_C_of_degree_le_one

added theorem polynomial.eval_map

modified theorem polynomial.eval_pow

added theorem polynomial.eval₂_hom

added theorem polynomial.eval₂_map

added theorem polynomial.exists_root_of_degree_eq_one

added theorem polynomial.leading_coeff_map

added theorem polynomial.map_div

added theorem polynomial.map_div_by_monic

added theorem polynomial.map_eq_zero

added theorem polynomial.map_id

added theorem polynomial.map_map

added theorem polynomial.map_mod

added theorem polynomial.map_mod_by_monic

added theorem polynomial.map_mod_div_by_monic

added theorem polynomial.map_neg

added theorem polynomial.map_sub

added theorem polynomial.monic_map

modified theorem polynomial.nat_degree_eq_of_degree_eq

added theorem polynomial.nat_degree_map

added theorem polynomial.ne_zero_of_monic_of_zero_ne_one