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 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
Showing 2,023 to 2,028 of 2,569 results.
ps_exists_qy_of_cancel
Mathematical 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
Mathematical 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
Mathematical 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.
ps_resultant_dvd_pow_eval_y
Mathematical statement
If B(X, y) = Q · A(X, y), then (X - y)^(degreeX A) divides the swapped resultant.
Source project: ArkLib
Person-level attribution pending.
ps_resultant_map
Mathematical statement
The resultant commutes with ring homomorphisms.
Source project: ArkLib
Person-level attribution pending.
ps_resultant_ne_zero_of_is_rel_prime
Mathematical statement
The resultant of relatively prime polynomials is nonzero.
Source project: ArkLib
Person-level attribution pending.