Right but there isn't a theorem saying `(sqrt x)^2 = x`, there's a theorem sayin... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		sebzim4500 78 days ago \| parent \| context \| favorite \| on: Some Junk Theorems in Lean Right but there isn't a theorem saying `(sqrt x)^2 = x`, there's a theorem saying `x >= 0 -> (sqrt x)^2 = x`

munchler 78 days ago [–]

Ah, that makes sense. Thank you. As long as every use of sqrt has such a condition.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact