Zulip Chat Archive

Stream: new members

Topic: 1/2 > 0


view this post on Zulip Debendro Mookerjee (Apr 01 2020 at 15:15):

How do you prove that 1/2 > 0
?

view this post on Zulip Reid Barton (Apr 01 2020 at 15:15):

(a) the norm_num tactic; (b) it might not be true.

view this post on Zulip Johan Commelin (Apr 01 2020 at 15:18):

@Debendro Mookerjee This depends on where the division takes place...

view this post on Zulip Johan Commelin (Apr 01 2020 at 15:18):

1/2 = 0 in the natural numbers.

view this post on Zulip Debendro Mookerjee (Apr 01 2020 at 15:20):

in the reals

view this post on Zulip Kenny Lau (Apr 01 2020 at 15:20):

it should be half_pos iirc

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 15:43):

one_half_pos

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 16:36):

But the best answer is norm_num, a generic tactic which will prove any equality or inequality for explicit real numbers.


Last updated: May 16 2021 at 05:21 UTC