Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-17 09:19 3ee1071e

View on Github →

feat(data/polynomial): lemmas relating unit and irreducible with degree (#514)

Estimated changes

Modified algebra/ordered_group.lean

added theorem with_bot.coe_one

Modified algebra/ordered_ring.lean

Modified data/nat/basic.lean

added theorem nat.one_lt_iff_ne_zero_and_ne_one

added theorem nat.with_bot.add_eq_one_iff

added theorem nat.with_bot.add_eq_zero_iff

Modified data/nat/prime.lean

added theorem nat.prime.ne_one

Modified data/polynomial.lean

added theorem polynomial.X_ne_zero

added theorem polynomial.coeff_X_zero

added theorem polynomial.coeff_mul_X_zero

added theorem polynomial.coeff_zero_eq_eval_zero

added theorem polynomial.degree_eq_zero_of_is_unit

added theorem polynomial.degree_pos_of_ne_zero_of_nonunit

added theorem polynomial.div_by_monic_one

added theorem polynomial.irreducible_of_degree_eq_one

added theorem polynomial.is_unit_iff_degree_eq_zero

added theorem polynomial.mod_by_monic_X

added theorem polynomial.mod_by_monic_one

added theorem polynomial.monic_X

added theorem polynomial.nat_degree_eq_of_degree_eq_some

added theorem polynomial.nat_degree_mul_eq

added theorem polynomial.zero_le_degree_iff

Modified data/zmod/quadratic_reciprocity.lean

modified theorem quadratic_reciprocity_aux.prod_range_p_mul_q_filter_coprime_mod_p

modified theorem zmodp.fermat_little

modified def zmodp.legendre_sym

modified theorem zmodp.legendre_sym_eq_one_or_neg_one

modified theorem zmodp.legendre_sym_eq_pow

modified theorem zmodp.prod_range_prime_erase_zero

modified theorem zmodp.quadratic_reciprocity

modified theorem zmodp.wilsons_lemma

Modified ring_theory/associated.lean

added theorem associates.mk_one

added theorem associates.mk_pow

added theorem irreducible_of_prime

added theorem is_unit_int

added theorem is_unit_pow

added theorem nat.prime_iff_prime

added theorem nat.prime_iff_prime_int

added theorem not_prime_one

added theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul