Commit 2024-10-19 07:30 a5ac03c2

chore(Algebra/Module): split off NoZeroSMulDivisors (#17909) The definition of NoZeroSMulDivisors doesn't require us to know about modules. By splitting off this definition, we can streamline the downstream import graph a bit. In the process, generalize a few instances from Module to SMulWithZero. New files:

• NoZeroSMulDivisors/Defs.lean: definition and basic results that don't require Module
• NoZeroSMulDivisors/Basic.lean: basic results that require Module
• NoZeroSMulDivisors/Pi.lean: results on NoZeroSMulDivisors _ (_ -> _) that don't require Module
• NoZeroSMulDivisors/Prod.lean: results on NoZeroSMulDivisors _ (_ x _) that don't require Module