Commit 2021-12-09 03:56 ab316732

feat(data/finset/basic): val_le_iff_val_subset (#10603) I'm not sure if we have something like this already on mathlib. The application of val_le_of_val_subset that I have in mind is to deduce

theorem polynomial.card_roots'' {F : Type u} [field F]{p : polynomial F}(h : p ≠ 0)
{Z : finset F} (hZ : ∀ z ∈ Z, polynomial.eval z p = 0) : Z.card ≤ p.nat_degree

from polynomial.card_roots' If this approach seems right, I will send the proof of polynomial.card_roots'' in a follow up PR.