Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-11 21:21 1c2b7420

View on Github →

feat(ring_theory/polynomial/cyclotomic/eval): cyclotomic_pos (#10482)

Estimated changes

Modified counterexamples/cyclotomic_105.lean

Modified src/data/nat/basic.lean

added theorem nat.two_lt_of_ne

Modified src/number_theory/primes_congruent_one.lean

Renamed src/ring_theory/polynomial/cyclotomic.lean to src/ring_theory/polynomial/cyclotomic/basic.lean

deleted theorem polynomial.eval_one_cyclotomic_prime

deleted theorem polynomial.eval_one_cyclotomic_prime_pow

deleted theorem polynomial.eval₂_one_cyclotomic_prime

deleted theorem polynomial.eval₂_one_cyclotomic_prime_pow

added theorem polynomial.prod_cyclotomic_eq_geom_sum

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

added theorem polynomial.cyclotomic_pos

added theorem polynomial.eval_one_cyclotomic_prime

added theorem polynomial.eval_one_cyclotomic_prime_pow

added theorem polynomial.eval₂_one_cyclotomic_prime

added theorem polynomial.eval₂_one_cyclotomic_prime_pow