Zulip Chat Archive

Stream: general

Topic: int order

Patrick Massot (Sep 13 2018 at 14:22):

Why is most of https://github.com/leanprover/mathlib/blob/master/data/int/order.lean commented out? Do we have these theorems elsewhere?

Patrick Massot (Sep 13 2018 at 14:23):

Do we usually keep commented code in mathlib?

Patrick Massot (Sep 13 2018 at 14:24):

Oh, it seems we have them in core :open_mouth:

Patrick Massot (Sep 13 2018 at 14:24):

@Mario Carneiro what's this mess?

Mario Carneiro (Sep 13 2018 at 14:34):

that is a very old file, ported from lean 2 I guess, and the theorems in it were either never updated or never needed, or appeared in other places (e.g. core) so they just stayed as is

Mario Carneiro (Sep 13 2018 at 14:35):

I'm pretty sure the whole file can be deleted

Mario Carneiro (Sep 13 2018 at 14:36):

on the plus side, it's good to see that the VSCode highlighting now understands that it is a comment; it used to try highlighting it since the nested comment at the start confused it

Patrick Massot (Sep 13 2018 at 14:36):

github highlighting doesn't

Mario Carneiro (Sep 13 2018 at 14:37):

theorem coe_nat_pos {n : ℕ} (Hpos : #nat n > 0) : ↑n > 0 :=

we haven't had that notation since lean 2

Mario Carneiro (Sep 13 2018 at 14:39):

I wanted to make sure that all the theorems in the file have equivalents before deleting it

Patrick Massot (Sep 13 2018 at 14:40):

Yeah, let's do that before Lean 4

Mario Carneiro (Sep 13 2018 at 14:41):

is that an exercise I can outsource?

Patrick Massot (Sep 13 2018 at 14:41):

It depends whether you're currently working on maths or the theory of computability of ordinal stuff :-p

Mario Carneiro (Sep 13 2018 at 14:46):

does linear algebra count as maths?

Patrick Massot (Sep 13 2018 at 14:46):

Is it over a semiring?

Mario Carneiro (Sep 13 2018 at 14:47):

lattice of submodules

Mario Carneiro (Sep 13 2018 at 14:47):

no semirings

Patrick Massot (Sep 13 2018 at 14:47):

I'm sure there is a trick, but let's say yes

Mario Carneiro (Sep 13 2018 at 14:47):

Since I agree that semimodules have dubious worth, I plan to only generalize theorems from modules as needed

Kevin Buzzard (Sep 13 2018 at 14:50):

Chris asked me if semifields existed yesterday. I asked him if every semiring could be embedded into a ring and he said he didn't think so, so I told him I had no clue what a semifield was. He suggested that you take the field axioms and then remove all the ones mentioning -. I suppose that's one way of making new structures! I wasn't even sure if this gave a well-defined definition (in the sense that there might be more than one way of axiomatising fields)

Bryan Gin-ge Chen (Sep 13 2018 at 14:50):

github highlighting doesn't

There's an open PR to fix the github highlighting; it probably needs to be updated for the most recent fixes to the VS code extension though.

Johan Commelin (Sep 13 2018 at 14:52):

Wow, this thread is degenerating quickly :lol:

Chris Hughes (Sep 13 2018 at 15:18):

PRed https://github.com/leanprover/mathlib/pull/348

Kevin Buzzard (Sep 13 2018 at 15:23):

me and Kenny are playing multiplayer lean

Kevin Buzzard (Sep 13 2018 at 15:23):

lots of things are there that weren't there last week. I should take this to the cocalc thread

Patrick Massot (Sep 13 2018 at 16:06):

Do we already have {α : Type*} [linear_ordered_ring α] {a : α} (h : a ≠ 0) : a * a > 0. I can prove it but it should be there already

Reid Barton (Sep 13 2018 at 16:11):

I guess it should have a name like mul_self_pos, and I don't see it.

Mario Carneiro (Sep 13 2018 at 16:12):

I don't think it's there, and it's good to have

Kevin Buzzard (Sep 13 2018 at 16:12):

There's mul_pos and mul_self_nonneg but maybe you found a hole :-)

Patrick Massot (Sep 13 2018 at 16:14):

Indeed I called it mul_self_pos.

Mario Carneiro (Sep 13 2018 at 16:14):

approve

Patrick Massot (Sep 13 2018 at 16:14):

Mario, do you want a PR or would it be quicker for you to add it yourself?

Patrick Massot (Sep 13 2018 at 16:28):

A PR would contains something like:

section linear_ordered_ring
variables {α : Type*} [linear_ordered_ring α]

lemma mul_self_eq_zero_iff (a : α) : a*a = 0 ↔ a = 0 :=
begin
  split; intro h,
  { cases linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero h with H H ; exact H },
  { rw [h, mul_zero] }
end

lemma mul_self_pos {a : α} (h : a ≠ 0) : a * a > 0 :=
lt_of_le_of_ne (mul_self_nonneg a) (λ H, h $ (mul_self_eq_zero_iff a).1 $ eq.symm H)
end linear_ordered_ring