mmh I'd don't say that much, I think the logic and math foundations is common in both classic and quantum theories, only content changing, so you would say "import mathlib" from both classic-phys.lean and quant-phys.lean if writing Lean proof assistant code (I am guessing the "import" command). Concepts from linear algebra as eigendecomposition, to say something, will be used in both applications.