mathlib3

2c28ce03 - feat(algebra/module/pi): Non-dependent shortcut (#17536)

feat(algebra/module/pi): Non-dependent shortcut (#17536) Without this special case instance, Lean can't synthesize `no_zero_smul_divisors ℝ (ι → ℝ)` in #2819.