Zulip Chat Archive

Stream: maths

Topic: no_zero_divisors definition


view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 09:14):

What do you think about making no_zero_divisors extend mul_zero_class?

view this post on Zulip Johan Commelin (Apr 07 2020 at 09:20):

I think I had a similar wish during the group_with_zero PR

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 09:23):

Let's see if someone objects.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 07 2020 at 09:24):

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

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 09:24):

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

view this post on Zulip 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×0\times\infty so it will be assigned a junk value anyway.

view this post on Zulip Scott Morrison (Apr 07 2020 at 09:26):

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

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 09:26):

and the answer is 0 :-)

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 09:28):

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

view this post on Zulip Mario Carneiro (Apr 07 2020 at 09:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 09:29):

But isn't this a different multiplication?

view this post on Zulip Mario Carneiro (Apr 07 2020 at 09:29):

it's just like multiplicative nat

view this post on Zulip Alex J. Best (Apr 07 2020 at 09:29):

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

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 09:29):

Is it a no_zero_divisors?

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 09:30):

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

view this post on Zulip Alex J. Best (Apr 07 2020 at 09:31):

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

view this post on Zulip Johan Commelin (Apr 07 2020 at 09:31):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 07 2020 at 09:38):

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

view this post on Zulip 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