mathlib

64fa9a20 - chore(*): futureproof import syntax (#2402)

chore(*): futureproof import syntax (#2402) The next community version of Lean will treat a line starting in the first column after an import as a new command, not a continuation of the import.