mathlib3
f6ccb6b8 - chore(ring_theory/polynomial/cyclotomic): golf+remove `nontrivial` (#9090)

Commit

4 years ago

chore(ring_theory/polynomial/cyclotomic): golf+remove `nontrivial` (#9090)

Author

ericrbg

ericrbg

Parents

Loading