# Zulip Chat Archive

## 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