Checking if a module is transitively imported

Stream: general

[Eric Wieser]

Is the a way to check if a module is imported in the current file? Obviously for direct imports I can look at the top, but what can I do for transitive imports?

[Kevin Buzzard]

I just do #check (some lemma in the file)