Zulip Chat Archive
Stream: general
Topic: squares
Patrick Massot (May 29 2018 at 21:38):
Do we have that the square of a real number is nonnegative?
Kenny Lau (May 29 2018 at 21:39):
mul_self_nonneg
Patrick Massot (May 29 2018 at 21:40):
looks promising
Patrick Massot (May 29 2018 at 21:41):
too bad x^2 is not defeq x*x :disappointed:
Last updated: May 02 2025 at 03:31 UTC