Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 3 research declarations. Search 10,000 more complete Mathlib declarations.
3 results
Clear filterscard_filter_eval_subtype_eq_piFinset
Plain-language statement
The number of elements in ā i, ā„(S i) satisfying eval (āĀ·) f = 0 equals the number of elements in Fintype.piFinset (fun i => (S i).toFinset) satisfying eval Ā· f = 0.
Source project: ArkLib
Person-level attribution pending.
prob_eval_zero_le_div
Plain-language statement
Probability of a nonzero polynomial evaluating to zero over a uniform product distribution is at most d / m, where d bounds the total degree and m bounds below the cardinality of each factor. This bridges schwartz_zippel_counting with the probability formulation.
Source project: ArkLib
Person-level attribution pending.
schwartz_zippel_counting
Plain-language statement
For a nonzero multivariate polynomial f of total degree at most d, evaluated over a product of finite subsets of a field F, each of cardinality at least m, the number of roots is at most d / m multiplied by the side of the product set.
Source project: ArkLib
Person-level attribution pending.