Theorems · Theorem · commutative algebra
Polynomial.resultant_comm
∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ),
f.resultant g m n = (-1) ^ (m * n) * g.resultant f n mRes(f, g) = (-1)ᵐⁿ Res(g, f)
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites46
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Finsetproof · cited by 13,712
- Fintypeproof · cited by 7,736
- Polynomialstatement and proof · cited by 5,681
- Matrixproof · cited by 4,303
- mul_oneproof · cited by 3,885
- Equiv.symmproof · cited by 3,681
- Finset.univproof · cited by 3,473
- LE.le.transproof · cited by 3,151
- one_mulproof · cited by 2,841
- Unitsproof · cited by 2,804
Cited by11
Results whose statement or proof uses this declaration.
- Polynomial.resultant_zero_right_degproof · cited by 8
- Polynomial.resultant_add_right_degproof · cited by 3
- Polynomial.resultant_mul_leftproof · cited by 2
- Polynomial.resultant_C_mul_leftproof · cited by 2
- Polynomial.resultant_prod_rightproof · cited by 1
- Polynomial.resultant_zero_leftproof · cited by 1
- Polynomial.resultant_X_sub_C_pow_rightproof · cited by 1
- Polynomial.resultant_X_sub_C_rightproof · cited by 1
- Polynomial.resultant_add_mul_leftproof · cited by 1
- Polynomial.resultant_eq_prod_roots_subproof · cited by 1
- Polynomial.resultant_derivproof · cited by 0