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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersps_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.
ps_exists_qx_of_cancel
Plain-language statement
After cancellation in X, a large subset of evaluation points witnesses P = quot_y.
Source project: ArkLib
Person-level attribution pending.
ps_exists_qy_of_cancel
Plain-language statement
After cancellation in Y, a large subset of evaluation points witnesses P = quot_x.
Source project: ArkLib
Person-level attribution pending.
ps_nat_degree_resultant_le
Plain-language statement
The degree of resultant(B, A, n, m) is at most m · degX(B) + n · degX(A).
Source project: ArkLib
Person-level attribution pending.
ps_resultant_dvd_pow_eval_x
Plain-language statement
If B(x, Y) = Q · A(x, Y), then (X - x)^(natDegreeY A) divides resultant(B, A).
Source project: ArkLib
Person-level attribution pending.