Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-17 15:10 418c1168

View on Github →

feat(data/polynomial): degree_map (#517)

Estimated changes

Modified algebra/big_operators.lean

modified theorem finset.prod_hom

added theorem finset.sum_hom

Modified algebra/group.lean

added theorem inv.is_group_hom

added theorem is_group_hom.to_is_monoid_hom

Modified algebra/group_power.lean

Modified algebra/module.lean

Modified algebra/pi_instances.lean

added theorem prod.fst.is_group_hom

added theorem prod.fst.is_monoid_hom

added theorem prod.snd.is_group_hom

added theorem prod.snd.is_monoid_hom

Modified analysis/topology/infinite_sum.lean

Modified data/complex/basic.lean

Modified data/complex/exponential.lean

Modified data/dfinsupp.lean

Modified data/finsupp.lean

Modified data/multiset.lean

Modified data/nat/cast.lean

Modified data/polynomial.lean

added theorem polynomial.coeff_map

modified theorem polynomial.coeff_sum

added theorem polynomial.degree_map_eq

added theorem polynomial.degree_map_le

Modified data/real/ennreal.lean

Modified data/real/nnreal.lean

Modified data/zmod/quadratic_reciprocity.lean

Modified linear_algebra/basic.lean

Modified linear_algebra/direct_sum_module.lean