omitted some variables

leanprover-community · Nov 23, 2024 · 5ad630a · 5ad630a
1 parent 950a378
commit 5ad630a
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean
@@ -42,8 +42,7 @@ namespace Polynomial
 
 section greatestFactorOneSubNotDvd
 
-variable {R : Type*} [CommRing R] [Nontrivial R] [NoZeroDivisors R]
-variable (p : R[X]) (hp : p ≠ 0) (d : ℕ)
+variable {R : Type*} [CommRing R] (p : R[X]) (hp : p ≠ 0) (d : ℕ)
 
 /--
 Given a polynomial `p`, the factor `f` of `p` such that the product of `f` and