instance
definition
linearSmallBias_poly
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SAT.SmallBias on GitHub at line 78.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
75 intro n
76 exact linearFamily_length_bound n
77
78instance linearSmallBias_poly : HasPolySize linearSmallBias :=
79 ⟨linearFamily_poly_bound⟩
80
81end SAT
82end Complexity
83end IndisputableMonolith