Importing file listed twice on docs page

Stream: mathlib4

[Michael Stoll]

The docs page for Mathlib.Algebra.Order.Ring.CharZero lists Mathlib.Data.Nat.Choose.Bounds twice under "imported by".

[Richard Osborn]

That's because it is imported twice. Mathlib/Data/Nat/Choose/Bounds.lean#L7

[Michael Stoll]

It also imports Mathlib.Data.Nat.Cast.Order twice! Is there no linter for this?

[Richard Osborn]

The two imports were added separately in #9720 and #9749 and were likely merged at roughly the same time. Not familiar enough with CI to know how to lint for this.