Ne.mul

Stream: mathlib4

[Kevin Buzzard]

import Mathlib

def Ne.mul := @mul_ne_zero

example (a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := ha.mul hb

I thought this was kind of cool, is it something mathlib would like? It was the first proof I tried before using exact?.

[Kevin Buzzard]

Assuming it goes in and people want to keep mul_ne_zero does this then automatically end up on Jovan's list of duplicated lemmas?

[Eric Wieser]

You could use alias and then it would be easier to auto-exclude from any automation

[Floris van Doorn]

In general, we are happy to include aliases to support dot notation ("generalized projection notation"). The fact that this one doesn't mention zero irks me a bit, but I think this might be nice to have.

[Alex Meiburg]

You could do this for Ne.add too. (There is docs#add_ne_zero, but it's not what I expected. Something with [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] probably.)

[Kevin Buzzard]

yeah I agree that it not mentioning zero is a bit weird. But "a not something" and "b not something" implies "a*b not something" isn't going to have too many applications other than 0 (which is pretty common).

[Floris van Doorn]

docs#ENNReal.mul_ne_top comes to mind, but probably shows up less in (the non-analysis part of) FLT than in Carleson :-)

[Kevin Buzzard]

Oh that's a good find! Is Ne.mul\_0 a better name then?

[Jz Pan]

But isn't Ne.mul a ≠ b -> c ≠ d -> a * c ≠ b * d?

[Jz Pan]

Of course it's not correct in general

[Ruben Van de Velde]

That's why it doesn't need the name :)

[Kevin Buzzard]

I think "not correct in general" is a bit of an understatement" :-)

[Jovan Gerbscheid]

Kevin Buzzard said:

Assuming it goes in and people want to keep mul_ne_zero does this then automatically end up on Jovan's list of duplicated lemmas?

As @Eric Wieser said, If you use alias, on won't appear on the list of duplicate lemmas.