mathlib3

55d224c3 - feat(ring_theory/polynomial/cyclotomic/eval): golf, add lemmas (#18022)

feat(ring_theory/polynomial/cyclotomic/eval): golf, add lemmas (#18022) * Add `nat.le_self_pow`, `polynomial.sub_one_pow_totient_le_cyclotomic_eval`, `polynomial.cyclotomic_eval_le_add_one_pow_totient`, `polynomial.sub_one_pow_totient_lt_nat_abs_cyclotomic_eval`, `zmod.order_of_units_dvd_card_sub_one`, and `zmod.order_of_dvd_card_sub_one`. * Rename `polynomial.cyclotomic_eval_lt_sub_one_pow_totient` to `polynomial.cyclotomic_eval_lt_add_one_pow_totient`. * Replace `nat.exists_prime_ge_modeq_one` with `nat.exists_prime_gt_modeq_one`. * Assume `≠ 0` instead of `0 <` in `nat.exists_prime_ge_modeq_one` etc. * Golf some proofs. Mathlib 4 version: leanprover-community/mathlib4#1273