ring_division): add `polynomial.card_le_degree_of_subset_roots` (#10824)

Commit

3 years ago

feat(data/polynomial/ring_division): add `polynomial.card_le_degree_of_subset_roots` (#10824) Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>

Author

isadofschi

Parents

ec6d9a73

mathlib bd164c7f - feat(data/polynomial/ring_division): add `polynomial.card_le_degree_of_subset_roots` (#10824)

mathlib
bd164c7f - feat(data/polynomial/ring_division): add `polynomial.card_le_degree_of_subset_roots` (#10824)