mathlib3

024aef0b - feat(data/pi): provide `pi.mul_single` (#11849)

feat(data/pi): provide `pi.mul_single` (#11849) the additive version was previously called `pi.single`, to this requires refactoring existing code. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>