Theorems · Theorem · commutative algebra

Polynomial.UniversalFactorizationRing.jacobian_resentation

∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  (Polynomial.UniversalFactorizationRing.presentation m k hn p).jacobian =
    (-1) ^ n *
      (↑(Polynomial.UniversalFactorizationRing.factor₁ m k hn p)).resultant
        ↑(Polynomial.UniversalFactorizationRing.factor₂ m k hn p)

Defined in: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Cited by: 1 results in Mathlib
Foundations: Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites43

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
Algebraproof · cited by 11,388
Polynomialstatement and proof · cited by 5,681
Equiv.symmproof · cited by 3,681
TensorProductproof · cited by 2,545
Nontrivialproof · cited by 2,416
MvPolynomialproof · cited by 2,140
map_mulproof · cited by 1,137
Polynomial.natDegreestatement and proof · cited by 1,105
Polynomial.coeffstatement · cited by 1,045
RingHom.compproof · cited by 899

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂proof · cited by 1