Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-24 03:58 452c9a29

View on Github →

feat(data/polynomial): nat_degree_comp (#477)

Estimated changes

Modified algebra/group_power.lean

added theorem add_monoid.smul_le_smul

added theorem add_monoid.smul_le_smul_of_le_right

added theorem with_bot.coe_smul

Modified algebra/ordered_group.lean

added theorem with_bot.coe_zero

modified theorem with_top.coe_add

Modified data/polynomial.lean

added theorem polynomial.coeff_comp_degree_mul_degree

added theorem polynomial.leading_coeff_comp

added theorem polynomial.nat_degree_comp

added theorem polynomial.nat_degree_comp_le

added theorem polynomial.nat_degree_one

added theorem polynomial.nat_degree_pow_eq'

added theorem polynomial.nat_degree_pow_eq