Linter complains about porting note before docstring

Stream: mathlib4

[zbatt]

In this commit, the linter seemed to be upset that I was putting a comment before the docstring. Is there a way around this or maybe I'm misinterpretting why the linter isn't passing?

[Kevin Buzzard]

This isn't the first time I've seen this. I would just delete the commented-out import.

[zbatt]

will do