Comment on Some Junk Theorems in LeanparentComments−munchler8moIf sqrt -1 = 0, then (by squaring both sides) -1 = 0, which is clearly unsound.−sebzim45008moRight but there isn't a theorem saying `(sqrt x)^2 = x`, there's a theorem saying `x >= 0 -> (sqrt x)^2 = x`−munchler8moAh, that makes sense. Thank you. As long as every use of sqrt has such a condition.
Comments
If sqrt -1 = 0, then (by squaring both sides) -1 = 0, which is clearly unsound.
Right but there isn't a theorem saying `(sqrt x)^2 = x`, there's a theorem saying `x >= 0 -> (sqrt x)^2 = x`
Ah, that makes sense. Thank you. As long as every use of sqrt has such a condition.