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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersps_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.
ps_sylvester_mul_vec_eq_coeff_add
Plain-language statement
The Sylvester matrix–vector product gives coefficients of A * P + B * Q.
Source project: ArkLib
Person-level attribution pending.