Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-10 10:39 ed4c536a

View on Github →

feat(data/polynomial): multiplicity of roots of polynomials (#656)

feat(data/polynomial): multiplicity of roots of polynomials
rename lemmas
use section
use nonzero_comm_ring.of_ne
refactor(polynomial): weaken decidablility hypothesis
indentation
swap order of arguments

Estimated changes

Modified src/algebra/ring.lean

added def nonzero_comm_ring.of_ne

Modified src/data/polynomial.lean

added def polynomial.decidable_dvd_monic

added theorem polynomial.div_by_monic_mul_pow_root_multiplicity_eq

added theorem polynomial.eval_div_by_monic_pow_root_multiplicity_ne_zero

added theorem polynomial.monic_mul

added theorem polynomial.monic_pow

added theorem polynomial.multiplicity_X_sub_C_finite

added theorem polynomial.multiplicity_finite_of_degree_pos_of_monic

added def polynomial.nonzero_comm_ring.of_polynomial_ne

added theorem polynomial.pow_root_multiplicity_dvd

added def polynomial.root_multiplicity

added theorem polynomial.root_multiplicity_eq_multiplicity