Zulip Chat Archive
Stream: new members
Topic: 1/2 > 0
Debendro Mookerjee (Apr 01 2020 at 15:15):
How do you prove that 1/2 > 0
?
Reid Barton (Apr 01 2020 at 15:15):
(a) the norm_num tactic; (b) it might not be true.
Johan Commelin (Apr 01 2020 at 15:18):
@Debendro Mookerjee This depends on where the division takes place...
Johan Commelin (Apr 01 2020 at 15:18):
1/2 = 0 in the natural numbers.
Debendro Mookerjee (Apr 01 2020 at 15:20):
in the reals
Kenny Lau (Apr 01 2020 at 15:20):
it should be half_pos iirc
Yury G. Kudryashov (Apr 01 2020 at 15:43):
one_half_pos
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: Dec 20 2023 at 11:08 UTC