## Stream: maths

### Topic: no_zero_divisors definition

#### Yury G. Kudryashov (Apr 07 2020 at 09:14):

What do you think about making no_zero_divisors extend mul_zero_class?

#### Johan Commelin (Apr 07 2020 at 09:20):

I think I had a similar wish during the group_with_zero PR

#### Yury G. Kudryashov (Apr 07 2020 at 09:23):

Let's see if someone objects.

#### Johan Commelin (Apr 07 2020 at 09:23):

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

#### Johan Commelin (Apr 07 2020 at 09:24):

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

#### Yury G. Kudryashov (Apr 07 2020 at 09:24):

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

#### Kevin Buzzard (Apr 07 2020 at 09:25):

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 (Apr 07 2020 at 09:26):

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

#### Kevin Buzzard (Apr 07 2020 at 09:26):

and the answer is 0 :-)

#### Kevin Buzzard (Apr 07 2020 at 09:27):

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 (Apr 07 2020 at 09:28):

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

#### Mario Carneiro (Apr 07 2020 at 09:28):

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

#### Kevin Buzzard (Apr 07 2020 at 09:28):

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 (Apr 07 2020 at 09:28):

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 (Apr 07 2020 at 09:29):

But isn't this a different multiplication?

#### Mario Carneiro (Apr 07 2020 at 09:29):

it's just like multiplicative nat

#### Alex J. Best (Apr 07 2020 at 09:29):

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

#### Yury G. Kudryashov (Apr 07 2020 at 09:29):

Is it a no_zero_divisors?

#### Kevin Buzzard (Apr 07 2020 at 09:30):

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

#### Alex J. Best (Apr 07 2020 at 09:31):

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

#### Johan Commelin (Apr 07 2020 at 09:31):

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

#### Johan Commelin (Apr 07 2020 at 09:31):

Alex J. Best said:

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

Yeah, that's a problem

#### Alex J. Best (Apr 07 2020 at 09:32):

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 (Apr 07 2020 at 09:33):

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

#### Johan Commelin (Apr 07 2020 at 09:34):

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

#### Mario Carneiro (Apr 07 2020 at 09:36):

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 (Apr 07 2020 at 09:37):

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 (Apr 07 2020 at 09:38):

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

#### Mario Carneiro (Apr 07 2020 at 09:39):

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

Last updated: May 18 2021 at 08:14 UTC