Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.wallis.le_W

Modification history

2023-01-26 09:46

src/data/real/pi/wallis.lean

feat(data/real/pi): refactor Wallis formula for pi (#18280) …

Added real.wallis.le_W View on Github →