mathlib3

9b94375a - feat(data/real/pi): refactor Wallis formula for pi (#18280)

feat(data/real/pi): refactor Wallis formula for pi (#18280) This is preparation for adding Euler's sine product (whose proof is a generalisation of the proof of Wallis' formula)