ref mathlib prs

BoltonBailey · May 19, 2024 · 091aefd · 091aefd
1 parent aabafbb
commit 091aefd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/FormalSnarksProject/ToMathlib/ForTransformations.lean b/FormalSnarksProject/ToMathlib/ForTransformations.lean
@@ -55,6 +55,7 @@ theorem MvPolynomial.degreeOf_C_mul {σ R : Type} [Field R] (j : σ)
     simp only [one_div, ne_eq, hc, not_false_eq_true, inv_mul_cancel, map_one, one_mul] at this
     convert this
 
+-- https://github.com/leanprover-community/mathlib4/pull/13024
 @[simp]
 lemma MvPolynomial.coeff_single_X {R : Type} {σ : Type u_1} [CommSemiring R] [DecidableEq σ]
     (j : σ) (n : ℕ)
@@ -65,6 +66,7 @@ lemma MvPolynomial.coeff_single_X {R : Type} {σ : Type u_1} [CommSemiring R] [D
   simp_rw [eq_iff_iff]
   tauto
 
+-- https://github.com/leanprover-community/mathlib4/pull/13024
 @[simp]
 lemma MvPolynomial.coeff_single_X_pow {R : Type} {σ : Type u_1} [CommSemiring R] [DecidableEq σ]
     (j : σ) (n k : ℕ)