Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 17:00 14d99a37

View on Github →

hotfix(data/real/irrational): cast problem

Estimated changes

modified theorem irr_sqrt_two