⚠ [8558/8560] Built ResidueConductor.Basic (4.4s)
warning: ResidueConductor/Basic.lean:65:8: This simp argument is unused:
  Nat.nsmul_eq_mul

Hint: Omit it from the simp argument list.
  simp ̵[̵N̵a̵t̵.̵n̵s̵m̵u̵l̵_̵e̵q̵_̵m̵u̵l̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8559/8560] Built ResidueConductor (3.2s)
Build completed successfully (8560 jobs).
