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: Dec 20 2023 at 11:08 UTC