mathlib3
c8edd608 - chore(data/polynomial/ring_division): golf a few proofs (#14097)

Commit
3 years ago
chore(data/polynomial/ring_division): golf a few proofs (#14097) * add `polynomial.finite_set_of_is_root`; * use it to golf a few proofs.
Author
Parents
Loading