chore: forward-port leanprover-community/mathlib#19084 (file 1 of 2) (#…

…4820)

[`linear_algebra.free_module.pid`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`d87199d51218d36a0a42c66c82d147b5a7ff87b3`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/free_module/pid?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..d87199d51218d36a0a42c66c82d147b5a7ff87b3)



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/LinearAlgebra/FreeModule/PID.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 
 ! This file was ported from Lean 3 source module linear_algebra.free_module.pid
-! leanprover-community/mathlib commit 210657c4ea4a4a7b234392f70a3a2a83346dfa90
+! leanprover-community/mathlib commit d87199d51218d36a0a42c66c82d147b5a7ff87b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -623,6 +623,9 @@ theorem Ideal.smithCoeffs_ne_zero (b : Basis ι R S) (I : Ideal S) (hI : I ≠ 
   simp [hi]
 #align ideal.smith_coeffs_ne_zero Ideal.smithCoeffs_ne_zero
 
+-- porting note: can be inferred in Lean 4 so no longer necessary
+#noalign has_quotient.quotient.module
+
 end Ideal
 
 end SmithNormal