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 8 research declarations. Search 10,000 more complete Mathlib declarations.
8 results
Clear filtersBerlekampWelch.linsolve_always_some_berlekamp_welch
Plain-language statement
If only up to e errors happened linsolve cannot fail to find a solution.
Source project: ArkLib
Person-level attribution pending.
BerlekampWelch.Q'_div_E'_eq_p
Plain-language statement
If there has happened up to e errors then any other E' and Q' satifying Berlekamp-Welch condition will result in the same quotient Q' \ E' = p.
Source project: ArkLib
Person-level attribution pending.
ps_coprime_case_constant
Plain-language statement
If A and B are coprime and agree on sufficiently many lines, then A is constant.
Source project: ArkLib
Person-level attribution pending.
ps_exists_p
Plain-language statement
Main existence: if B/A agrees with low-degree quotients on enough lines, then A ∣ B.
Source project: ArkLib
Person-level attribution pending.
ps_exists_p_nonzero
Plain-language statement
Existence of P with B = P * A when both A and B are nonzero.
Source project: ArkLib
Person-level attribution pending.
ps_exists_p_of_degree_x_eq_zero_nat_degree_y_eq_zero
Plain-language statement
A bivariate polynomial of degree zero in both variables divides every polynomial.
Source project: ArkLib
Person-level attribution pending.