Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.of_near

Modification history

2018-01-21 23:57

feat(data/real): real square root function, sqrt 2 is irrational

Added real.of_near View on Github →