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 7 research declarations. Search 10,000 more complete Mathlib declarations.
7 results
Clear filtersps_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.
ps_resultant_dvd_pow_eval_y
Plain-language 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
Plain-language statement
The resultant commutes with ring homomorphisms.
Source project: ArkLib
Person-level attribution pending.
ps_resultant_ne_zero_of_is_rel_prime
Plain-language statement
The resultant of relatively prime polynomials is nonzero.
Source project: ArkLib
Person-level attribution pending.
ps_sylvester_map
Plain-language statement
The Sylvester matrix commutes with ring homomorphisms.
Source project: ArkLib
Person-level attribution pending.