mathlib3
d6e1c554 - chore(data/polynomial/monic): dedup `degree_map` (#11792)

Commit

3 years ago

chore(data/polynomial/monic): dedup `degree_map` (#11792)

Author

ericrbg

ericrbg

Parents

Loading