Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-16 12:31 83490903

View on Github →

feat(ring_theory/polynomial/cyclotomic): generalize some lemmas to [ring R] (#17555)

Generalize some lemmas from commutative (semi)rings to (semi)rings.
Use finset.erase s 1 instead of s \ {1}.

Estimated changes

Modified archive/100-theorems-list/37_solution_of_cubic.lean

Modified src/data/finset/basic.lean

added theorem finset.erase_insert_of_ne

Modified src/data/polynomial/eval.lean

modified theorem polynomial.map_dvd

Modified src/number_theory/divisors.lean

added theorem nat.one_mem_divisors

Modified src/number_theory/padics/padic_val.lean

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

modified theorem polynomial.cyclotomic.dvd_X_pow_sub_one

modified theorem polynomial.cyclotomic_dvd_geom_sum_of_dvd

deleted theorem polynomial.cyclotomic_eq_geom_sum

added theorem polynomial.cyclotomic_prime

modified theorem polynomial.cyclotomic_prime_mul_X_sub_one

modified theorem polynomial.cyclotomic_prime_pow_eq_geom_sum

added theorem polynomial.cyclotomic_three

modified theorem polynomial.prod_cyclotomic_eq_geom_sum

Modified src/ring_theory/polynomial/cyclotomic/eval.lean

Modified src/ring_theory/polynomial/eisenstein.lean