Zulip Chat Archive

Stream: general

Topic: nat.pos_iff_ne_zero'


view this post on Zulip Reid Barton (Oct 24 2019 at 14:58):

From data.nat.basic:

theorem pos_iff_ne_zero : 0 < n  n  0 :=
ne_of_gt, nat.pos_of_ne_zero

theorem pos_iff_ne_zero' : 0 < n  n  0 := pos_iff_ne_zero

Anyone understand the purpose of this?

view this post on Zulip Johan Commelin (Oct 24 2019 at 15:01):

rotflol

view this post on Zulip Bryan Gin-ge Chen (Oct 24 2019 at 15:01):

Looks like pos_iff_ne_zero originally had n > 0 until #1436.

view this post on Zulip Johan Commelin (Oct 24 2019 at 15:03):

Aha, that makes sense

view this post on Zulip Johan Commelin (Oct 24 2019 at 15:04):

src/analysis/complex/exponential.lean:have hn0 : (n : ℝ) ≠ 0, by simpa [nat.pos_iff_ne_zero'] using hn,
src/data/nat/basic.lean:theorem pos_iff_ne_zero' : 0 < n ↔ n ≠ 0 := pos_iff_ne_zero
src/data/nat/basic.lean:by have := @size_pos n; simp [pos_iff_ne_zero'] at this;
src/ring_theory/multiplicity.lean:  rw [finite_int_iff_nat_abs_finite, finite_nat_iff, nat.pos_iff_ne_zero'],

view this post on Zulip Reid Barton (Oct 24 2019 at 18:57):

#1610

view this post on Zulip Johan Commelin (Oct 24 2019 at 19:00):

It's in the hands of Travis now... :thinking:


Last updated: May 10 2021 at 00:31 UTC