## Stream: general

### Topic: nonzero_ring?

#### Kenny Lau (May 27 2020 at 08:51):

We have nonzero_comm_ring and nonzero_comm_semiring and nonzero_semiring but not nonzero_ring. Is this deliberate?

Probably not

#### Kenny Lau (May 27 2020 at 08:57):

/-- Predicate for semirings in which zero does not equal one. -/
class nonzero_semiring (α : Type*) extends semiring α, zero_ne_one_class α

/-- Predicate for commutative semirings in which zero does not equal one. -/
class nonzero_comm_semiring (α : Type*) extends comm_semiring α, zero_ne_one_class α

/-- Predicate for commutative rings in which zero does not equal one. -/
class nonzero_comm_ring (α : Type*) extends comm_ring α, zero_ne_one_class α


#### Kenny Lau (May 27 2020 at 09:00):

https://github.com/leanprover-community/mathlib/pull/2595/files#diff-997c56fe87e1352880681d783e610a7f

#### Kenny Lau (May 27 2020 at 09:00):

#2595 created nonzero_semiring but not nonzero_ring

#2839

#### Chris Hughes (May 27 2020 at 10:43):

The point of the commutative versions was to deal with polynomials. Nobody's found a point of the non commutative versions yet.

#### Chris Hughes (May 27 2020 at 10:44):

Is this related to codewars? I wanted this class for a Kata.

#### Kenny Lau (May 27 2020 at 10:47):

no, I want to refactor linear_algebra.basic

#### Kenny Lau (May 27 2020 at 10:47):

there are a lot of theorems with rings and 0 ne 1 assumption

#### Johan Commelin (May 27 2020 at 10:48):

Shouldn't zero_ne_one_class be a prop?

#### Johan Commelin (May 27 2020 at 10:49):

We could have a class [nonzero R], and then we can get rid of nonzero_* for all versions of *.

#### Mario Carneiro (May 27 2020 at 10:49):

zero_ne_one_class is one of the things we need to delete

#### Mario Carneiro (May 27 2020 at 10:50):

it makes sense for an algebraic hierarchy that isn't mathlib's

#### Mario Carneiro (May 27 2020 at 10:51):

If you use mixins for making classes, a la the mathcomp hierarchy, it makes sense

#### Kevin Buzzard (May 27 2020 at 10:54):

We want a non_subsingleton class :-)

#### Mario Carneiro (May 27 2020 at 10:55):

are those always the same thing in all classes where zero_ne_one makes sense?

#### Mario Carneiro (May 27 2020 at 10:56):

I guess it's true as long as 0 * x = 0 and 1 * x = x

#### Mario Carneiro (May 27 2020 at 10:57):

which seem like pretty safe bets in an algebraic class with a thing called 0

#### Johan Commelin (May 27 2020 at 10:57):

Is it true in with_zero \a if \a is an ordered_add_comm_monoid?

#### Johan Commelin (May 27 2020 at 10:57):

To bad... we don't have a 1 there :sad:

#### Kevin Buzzard (May 27 2020 at 10:58):

so 1 is definitely not 0, because we have two of those!

#### Mario Carneiro (May 27 2020 at 10:58):

It's not true in a add_monoid has_one, which is the context where nat.cast is stated

#### Kevin Buzzard (May 27 2020 at 10:58):

Johan's class should be an instance of zero_ne_zero_class

#### Reid Barton (May 27 2020 at 11:00):

that's the to_additive of zero_ne_one_class right?

#### Mario Carneiro (May 27 2020 at 11:01):

I feel like it should be possible to to_additive a semiring and get a tropical ring

#### Johan Commelin (May 27 2020 at 11:02):

Back on topic: what do we do with nonzero_*?

#### Johan Commelin (May 27 2020 at 11:02):

I wouldn't want to waste Kenny's refactor energy

#### Mario Carneiro (May 27 2020 at 11:02):

I think your idea is a good one

#### Mario Carneiro (May 27 2020 at 11:04):

although I think that we should still have things like domain and field containing nonzero as part of the structure

#### Johan Commelin (May 27 2020 at 20:46):

@Mario Carneiro what do you think of just using [fact (0:R) ≠ 1] whenever we need it, and adding an instance for this fact for [domain R]?

#### Johan Commelin (May 27 2020 at 20:46):

Then we can remove all the nonzero_* classes completely

#### Mario Carneiro (May 27 2020 at 20:56):

You can do this kind of encoding for anything. The big downside is that all facts end up in a single class, which means that typeclass inference is going to have to sort through all facts in all contexts when trying to prove this. So no, I think we should try to not have any instances of fact other than local instances and hypotheses

#### Kenny Lau (May 27 2020 at 21:11):

so what should we do?

#### Mario Carneiro (May 27 2020 at 21:11):

have a nonzero R class, which was Johan's original suggestion

for semiring?

#### Mario Carneiro (May 27 2020 at 21:13):

class nonzero (R) [has_zero R] [has_one R] := (zero_ne_one : 0 != 1)

#### Mario Carneiro (May 27 2020 at 21:13):

it could also be class nonzero (R) [semiring R]

#### Mario Carneiro (May 27 2020 at 21:14):

do we have monoid_with_zero?

Yes we do

#### Mario Carneiro (May 27 2020 at 21:15):

ah, I should get in the habit of using that for stuff with 0 and 1

#### Johan Commelin (May 27 2020 at 21:15):

But a monoid_with_zero is always nonzero

#### Johan Commelin (May 27 2020 at 21:15):

So I vote for your first option

say what?

#### Mario Carneiro (May 27 2020 at 21:15):

that's definitely the wrong choice

#### Johan Commelin (May 27 2020 at 21:16):

Well, it worked for my one application...

#### Mario Carneiro (May 27 2020 at 21:16):

If monoid_with_zero is to group_with_zero as ring is to division_ring then it shouldn't have nonzero

#### Mario Carneiro (May 27 2020 at 21:17):

In particular I would like semirings to be monoid_with_zero

#### Johan Commelin (May 27 2020 at 21:17):

Yup, but I'm not sure that analogy should hold

#### Johan Commelin (May 27 2020 at 21:17):

Apparently in tropical geometry people study monoid_with_zero Ms and they are all nonzero by assumption.

#### Johan Commelin (May 27 2020 at 21:17):

That's why I included that assumption.

#### Johan Commelin (May 27 2020 at 21:17):

But it's probably a 2-line refactor to drop that assumption from mathlib

#### Mario Carneiro (May 27 2020 at 21:17):

luckily we now have a way to say this :)

#### Johan Commelin (May 27 2020 at 21:18):

s/now/almost/

#### Johan Commelin (May 27 2020 at 21:18):

I need to refill my 'refactor-mathlib' battery. So I would like to take a pass on this one.

#### Mario Carneiro (May 27 2020 at 21:18):

It seems awkward that group_with_zero and semiring currently have no greatest lower bound

#### Kevin Buzzard (May 27 2020 at 21:19):

The mathematical world is still reeling from the introduction of this new group_with_zero concept

#### Johan Commelin (May 27 2020 at 21:19):

But a complete refactor of the algebraic hierarchy... I wouldn't want to do that without more supporting tools

#### Kevin Buzzard (May 27 2020 at 21:19):

we haven't yet decided how much further it goes

#### Mario Carneiro (May 27 2020 at 21:20):

Johan Commelin said:

But a complete refactor of the algebraic hierarchy... I wouldn't want to do that without more supporting tools

It's not a complete refactor, just one new class

#### Mario Carneiro (May 27 2020 at 21:20):

some theorems will transfer to the weaker assumption, other stuff won't

#### Mario Carneiro (May 27 2020 at 21:20):

since it's a GLB class there will be no conflicts

#### Kenny Lau (May 28 2020 at 07:32):

Mario Carneiro said:

class nonzero (R) [has_zero R] [has_one R] := (zero_ne_one : 0 != 1)

#### Johan Commelin (May 28 2020 at 07:34):

Every sentence a verb

#### Johan Commelin (May 28 2020 at 07:35):

In other words: what the point?

#### Kenny Lau (May 28 2020 at 07:35):

I have started this refactor on the nonzero branch

#### Kenny Lau (May 28 2020 at 07:42):

[nonzero_semiring α] becomes [semiring α] [nonzero α]
[nonzero_comm_semiring α] becomes [comm_semiring α] [nonzero α]
[nonzero_comm_ring α] becomes [comm_ring α] [nonzero α]

#### Kenny Lau (May 28 2020 at 07:42):

(is there a place where I can put information like this?)

#### Johan Commelin (May 28 2020 at 07:43):

The commit message?

#### Bryan Gin-ge Chen (May 28 2020 at 07:45):

Note that when you make a PR, the contents of the first post become the commit message of the final squashed and merged commit.

#### Kenny Lau (May 28 2020 at 07:46):

along with the title?

#### Johan Commelin (May 28 2020 at 07:47):

When you create the PR it suggests a title, but it's usually crappy. It might also suggest a message, but you might want to change it.

#### Kenny Lau (May 28 2020 at 07:48):

I'm just asking whether the title also becomes the commit message

#### Kenny Lau (May 28 2020 at 07:48):

i.e. whether #2847 is correct

#### Johan Commelin (May 28 2020 at 07:48):

The title becomes the first line of the message, and will afterwards typically be formatted as a title.

#### Johan Commelin (May 28 2020 at 07:49):

Kenny Lau said:

i.e. whether #2847 is correct

Yup, looks fine to me

#### Kenny Lau (May 28 2020 at 07:50):

@[ancestor has_mul has_zero]
class no_zero_divisors (α : Type u) extends has_mul α, has_zero α :=
(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)


#### Kenny Lau (May 28 2020 at 07:50):

can we make this a Prop?

#### Kenny Lau (May 28 2020 at 07:50):

(by moving has_mul and has_zero before extends)

#### Kenny Lau (May 28 2020 at 07:50):

class domain (α : Type u) extends ring α, no_zero_divisors α, nonzero α


#### Kenny Lau (May 28 2020 at 07:51):

because the nonzero is problematic in "old_str_cmd true" and the no_zero_divisors is problematic in "false"

#### Johan Commelin (May 28 2020 at 07:51):

Yup, I would like that one to become a prop as well

#### Mario Carneiro (May 28 2020 at 07:51):

no_zero_divisors looks about as useful as zero_ne_one_class and distrib

Unbundling FTW!

#### Mario Carneiro (May 28 2020 at 07:52):

I think it should just be deleted (and merged into domain)

#### Johan Commelin (May 28 2020 at 07:52):

But group_with_zero!

#### Mario Carneiro (May 28 2020 at 07:53):

aha, is that a thing?

#### Johan Commelin (May 28 2020 at 07:53):

Never heard of them before

pre-domain

#### Johan Commelin (May 28 2020 at 07:54):

quasi-pseudo-demi-domain

#### Mario Carneiro (May 28 2020 at 07:54):

splitting semimonoid

#### Mario Carneiro (May 28 2020 at 07:54):

gotta keep them guessing

#### Kenny Lau (May 30 2020 at 06:55):

chore(algebra): displace zero_ne_one_class with nonzero and make no_z…
chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847)

• [nonzero_semiring α] becomes [semiring α] [nonzero α]
• [nonzero_comm_semiring α] becomes [comm_semiring α] [nonzero α]
• [nonzero_comm_ring α] becomes [comm_ring α] [nonzero α]
• no_zero_divisors is now a Prop
• units.ne_zero (originally for domain) merges into units.coe_ne_zero (originally for nonzero_comm_semiring)

#### Johan Commelin (May 30 2020 at 07:12):

Thanks @Kenny Lau

Last updated: May 15 2021 at 00:39 UTC