basic): ɸ_pⁱ irreducible → ɸ_pʲ irreducible for j ≤ i (#13952)

Commit

3 years ago

feat(polynomial/cyclotomic/basic): ɸ_pⁱ irreducible → ɸ_pʲ irreducible for j ≤ i (#13952) Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author

ericrbg

Parents

057e0283

mathlib3 8e0ab168 - feat(polynomial/cyclotomic/basic): ɸ_pⁱ irreducible → ɸ_pʲ irreducible for j ≤ i (#13952)

mathlib3
8e0ab168 - feat(polynomial/cyclotomic/basic): ɸ_pⁱ irreducible → ɸ_pʲ irreducible for j ≤ i (#13952)