Commit 2023-06-16 17:18 0bd86542

View on Github →

feat: port RingTheory.Polynomial.Cyclotomic.Eval (#5144)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

added theorem Polynomial.cyclotomic_eval_le_add_one_pow_totient

added theorem Polynomial.cyclotomic_eval_lt_add_one_pow_totient

added theorem Polynomial.cyclotomic_nonneg

added theorem Polynomial.cyclotomic_pos'

added theorem Polynomial.cyclotomic_pos

added theorem Polynomial.cyclotomic_pos_and_nonneg

added theorem Polynomial.eval_one_cyclotomic_not_prime_pow

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

added theorem Polynomial.sub_one_lt_natAbs_cyclotomic_eval

added theorem Polynomial.sub_one_pow_totient_le_cyclotomic_eval

added theorem Polynomial.sub_one_pow_totient_lt_cyclotomic_eval

added theorem Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval