Zulip Chat Archive

Stream: general

Topic: nat.pos_iff_ne_zero'

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?

Johan Commelin (Oct 24 2019 at 15:01):

rotflol

Bryan Gin-ge Chen (Oct 24 2019 at 15:01):

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

Johan Commelin (Oct 24 2019 at 15:03):

Aha, that makes sense

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'],

Reid Barton (Oct 24 2019 at 18:57):

#1610

Johan Commelin (Oct 24 2019 at 19:00):

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

Last updated: Dec 20 2023 at 11:08 UTC