Update Mathlib/RingTheory/Smooth/StandardSmooth.lean

Co-authored-by: Andrew Yang <[email protected]>
leanprover-community · Jan 7, 2025 · d752d6c · d752d6c
1 parent 2a19ed1
commit d752d6c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/Smooth/StandardSmooth.lean b/Mathlib/RingTheory/Smooth/StandardSmooth.lean
@@ -319,7 +319,7 @@ section P
 
 variable [Fintype P.rels] [DecidableEq P.rels]
 
-private lemma jacobiMatrix_comp_inr_inr  (i j : P.rels) :
+private lemma jacobiMatrix_comp_inr_inr (i j : P.rels) :
     (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) =
       MvPolynomial.rename Sum.inr (P.jacobiMatrix i j) := by
   rw [jacobiMatrix_apply, jacobiMatrix_apply]