Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.sqrt

Modification history

2020-12-16 13:55

src/data/real/sqrt.lean

refactor(data/real): move `real.sqrt` to `data.real.sqrt`, more dependencies (#5359) …

Added continuous.sqrt View on Github →