no_zero_divisors definition

Stream: maths

[Yury G. Kudryashov]

What do you think about making no_zero_divisors extend mul_zero_class?

[Johan Commelin]

I think I had a similar wish during the group_with_zero PR

[Yury G. Kudryashov]

Let's see if someone objects.

[Johan Commelin]

Can anyone cook up a natural algebraic structure that has_zero and has_mul but not mul_zero_class?

[Johan Commelin]

I think that all examples I've seen in my life satisfied 0 * x = 0

[Yury G. Kudryashov]

BTW, mul_eq_zero is an iff while mul_eq_zero' is not.

[Kevin Buzzard]

You can't even use a structure with "x=infinity" because there will be no mathematical sense to $0\times\infty$ so it will be assigned a junk value anyway.

[Scott Morrison]

cardinalities have a perfectly good 0 * \infty, where the value of 0 is not just junk

[Kevin Buzzard]

and the answer is 0 :-)

[Kevin Buzzard]

Is there a multiplication on these things like ereal and ennreal? I think I made ereal and I really fought hard against defining a multiplication on it.

[Yury G. Kudryashov]

There is a multiplication on ennreal, and it's useful. 0 * ∞ = 0.

[Mario Carneiro]

Also 0 times infinity is 0 in an extended nonnegative real measure

[Kevin Buzzard]

i figured that if the numbers were real then we already had a multiplication, and it was not my job to extend multiplication onto ereal by making arbitrary decisions about mathematically meaningless questions.

[Alex J. Best]

Well we're a long way from tropical semirings but depending on how the notation is set up I guess in the tropical semiring on real we have 0 * a = a

[Kevin Buzzard]

But isn't this a different multiplication?

[Mario Carneiro]

it's just like multiplicative nat

[Alex J. Best]

It is, which is what I mean by how the notation is set up.

[Yury G. Kudryashov]

Is it a no_zero_divisors?

[Kevin Buzzard]

On Wikipedia they don't use * notation for the tropical multiplication, they use $\otimes$

[Alex J. Best]

Sure, but if you're going to make it a semiring instance.

[Johan Commelin]

Right... so we should have has_tensor some time in the future (-;

[Johan Commelin]

Alex J. Best said:

Sure, but if you're going to make it a semiring instance.

Yeah, that's a problem

[Alex J. Best]

It all works nicely when 0 is the actual zero of the semiring -\infty but then you have two zeroes floating around...

[Alex J. Best]

In that case there's no zero divisors, but there are lots of \u (0 : \R) divisors.

[Johan Commelin]

I wonder if this a point where the "tie notation into the algebraic hierarchy" strategy is going to break down.

[Mario Carneiro]

Johan Commelin said:

Right... so we should have has_tensor some time in the future (-;

Wiat, so then does this mean there will be a tensor_ring? A to_tensor tactic that copies the library over to tensor rings?

[Johan Commelin]

Johan Commelin said:

I wonder if this a point where the "tie notation into the algebraic hierarchy" strategy is going to break down.

:up: @Mario Carneiro

[Mario Carneiro]

I know, I just wanted to underscore the point. This is obviously a bad idea

[Mario Carneiro]

I wouldn't object to has_tensor as a notation-only typeclass though