Theorems · Theorem · field theory
Polynomial.revAt_invol
∀ {N i : ℕ}, (Polynomial.revAt N) ((Polynomial.revAt N) i) = i- Defined in
- Mathlib.Algebra.Polynomial.Reverse
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Function.Embeddingstatement · cited by 988
- Polynomial.revAtstatement · cited by 26
- Polynomial.revAtFun_involproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- Polynomial.coeff_reflectproof · cited by 9
- Polynomial.reverse_leadingCoeffproof · cited by 5
- Polynomial.mirror_mirrorproof · cited by 5
- Polynomial.mirror_eval_oneproof · cited by 1
- Polynomial.reflect_reflectproof · cited by 1
- Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegreeproof · cited by 1
- Polynomial.coeff_mul_mirrorproof · cited by 1