# Zulip Chat Archive

## Stream: new members

### Topic: 1 mod 2 is in ℝ

#### Lars Ericson (Jan 21 2021 at 02:20):

Lean isn't letting me say this:

```
#check (1:zmod 2) ∈ {x : ℝ | ∃ (y : zmod 2), x = ↑y}
```

the complaint is

```
failed to synthesize type class instance for
⊢ has_mem (zmod 2) (set ℝ)
```

Is there a way to make this work?

#### Alex J. Best (Jan 21 2021 at 02:38):

It's not clear what mathematically 1 mod 2 in R is. There are no ring homomorphisms from Z/2 to R or even additive homomorphisms.

#### Adam Topaz (Jan 21 2021 at 03:53):

@Lars Ericson I made some assumptions about what you're actually trying to do.

```
import data.real.basic
#check (1 % 2) ∈ {r : ℝ | ∃ y : fin 2, r = y}
```

#### Damiano Testa (Jan 21 2021 at 05:17):

For me, one of the hardest concepts to internalise of type theory is that terms have a unique type. When you write `(1 : zmod 2)`

, you are explicitly saying what the type of `1`

is. Right after that, you are telling Lean that the term `1`

has type `\R`

. This cannot be, since terms have a unique type!

#### Lars Ericson (Jan 21 2021 at 05:36):

The context is that I am working on Exercise 7(a):

Screenshot-from-2021-01-21-00-28-17.png

I am trying to fill out this sketch:

```
import data.zmod.basic
import ring_theory.subring
import data.real.basic
import tactic
import tactic.slim_check
open real
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr -- Eric Wieser
instance foo: has_mem (zmod 2) (set ℝ) := sorry
theorem A_one : (1:zmod 2) ∈ {x : ℝ | ∃ (y : zmod 2), x = ↑y} :=
begin
sorry
end
def A : subring ℝ :=
{ carrier := {x : ℝ | ∃ (y : zmod 2), x = y},
one_mem' := A_one,
mul_mem' := sorry,
zero_mem' := sorry,
add_mem' := sorry,
neg_mem' := sorry,
}
theorem ex7a : is_an_integral_domain {x : ℝ | ∃ (y : zmod 2), x = y} :=
⟨A, infer_instance, rfl⟩
```

In other words I think `zmod 2`

is an integral domain and I am trying to adapt a proof pattern used previously to prove it.

#### Kyle Miller (Jan 21 2021 at 05:49):

You could take that as a recipe to construct a new number system with symbols `0`

and `1`

that behave in the described way -- they don't have to literally be `0`

and `1`

in the real numbers.

Here's a start at creating that number system, call it `R`

:

```
inductive R
| zero
| one
open R
def R.add : R → R → R
| zero zero := zero
| zero one := one
| one zero := one
| one one := zero
def R.mul : R → R → R
| zero zero := zero
| zero one := zero
| one zero := zero
| one one := one
instance : has_add R := ⟨R.add⟩
instance : has_mul R := ⟨R.mul⟩
instance : has_zero R := ⟨zero⟩
instance : has_one R := ⟨one⟩
```

#### Kyle Miller (Jan 21 2021 at 05:50):

Many proofs are trivial if you do them by cases:

```
lemma R_add_comm {a b : R} : a + b = b + a :=
begin
cases a; cases b; refl
end
```

#### Kyle Miller (Jan 21 2021 at 05:51):

Another:

```
lemma R_mul_one {a : R} : a * 1 = a :=
by { cases a; refl }
```

#### Kyle Miller (Jan 21 2021 at 05:51):

(The downside of course is that you don't inherit any of the structure of another number system. Just showing it can be done this way.)

#### Eric Wieser (Jan 21 2021 at 07:39):

Can't you just use zmod2 directly, rather than embedding it to the reals?

#### Lars Ericson (Jan 21 2021 at 15:06):

Thanks I will work through both @Kyle Miller sketch and @Eric Wieser suggestion of proving

```
instance : integral_domain (zmod 2)
```

I am working through Kyle's sketch now. One interesting point, not clear in the exercise, but which is required by `integral_domain`

, is to define `neg`

. There are two ways to go, one is `-0=0`

and `-1=1`

which conforms to `zmod 2`

. The other is `-0=1`

and `-1=0`

which corresponds to a Boolean algebra. I guess I'll try both and see if both `neg`

s give integral domains.

#### Eric Wieser (Jan 21 2021 at 15:15):

The proof amounts to "import the right files, remind mathlib that 2 is prime":

```
import data.nat.prime
import data.zmod.basic
instance : fact (nat.prime 2) := nat.prime_two
-- this is `@field.to_integral_domain _ (zmod.field 2)` under the hood
instance : integral_domain (zmod 2) := by apply_instance
```

I don't know if there's a more idiomatic way to introduce the `fact`

.

If you actually want to know what the proof is, rather than just knowing that we already have it, check out src#zmod.field

#### Adam Topaz (Jan 21 2021 at 15:58):

When you import `data.zmod.basic`

, I think you're automatically importing the ring structure on `zmod n`

as well. If you want to do the exercise of defining the addition, multiplication, etc. from scratch, I suggest following Kyle's approach above.

#### Mario Carneiro (Jan 21 2021 at 16:13):

Lars Ericson said:

One interesting point, not clear in the exercise, but which is required by

`integral_domain`

, is to define`neg`

. There are two ways to go, one is`-0=0`

and`-1=1`

which conforms to`zmod 2`

. The other is`-0=1`

and`-1=0`

which corresponds to a Boolean algebra. I guess I'll try both and see if both`neg`

s give integral domains.

The axioms of an integral domain (an additive group, even) require that `-0 = 0`

, so whatever element you decide to call zero has to be its own inverse. The complementation in a boolean algebra is not a valid group operation.

#### Lars Ericson (Jan 21 2021 at 23:26):

Done, following Kyle's approach:

```
import ring_theory.subring
import tactic
import tactic.slim_check
import data.zmod.basic
inductive R
| zero
| one
open R
def R.add : R → R → R
| zero zero := zero
| zero one := one
| one zero := one
| one one := zero
def R.mul : R → R → R
| zero zero := zero
| zero one := zero
| one zero := zero
| one one := one
def R.neg : R → R
| zero := zero
| one := one
instance : has_add R := ⟨R.add⟩
instance : has_mul R := ⟨R.mul⟩
instance : has_zero R := ⟨zero⟩
instance : has_one R := ⟨one⟩
instance : has_neg R := ⟨R.neg⟩
theorem R.exists_pair_ne : ∃ (x y : R), x ≠ y :=
begin
use [R.zero, R.one],
end
theorem R.zero_add (a : R): 0 + a = a :=
begin
cases a,
repeat { exact rfl },
end
theorem R.add_zero (a : R): a + 0 = a :=
begin
cases a,
repeat { exact rfl },
end
theorem R.one_mul (a : R): 1 * a = a :=
begin
cases a,
repeat { exact rfl },
end
theorem R.mul_one (a : R): a * 1 = a :=
begin
cases a,
repeat { exact rfl },
end
theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
cases a,
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
end
theorem R.add_left_neg (a : R): -a + a = 0 :=
begin
cases a,
repeat { exact rfl },
end
theorem R.add_comm (a b : R): a + b = b + a :=
begin
cases a,
cases b,
repeat { exact rfl },
cases b,
repeat { exact rfl },
end
theorem R.mul_assoc (a b c : R): a * b * c = a * (b * c) :=
begin
cases a,
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
end
theorem R.left_distrib (a b c : R): a * (b + c) = a * b + a * c :=
begin
cases a,
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
end
theorem R.right_distrib (a b c : R): (a + b) * c = a * c + b * c :=
begin
cases a,
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
cases b,
cases c,
repeat { exact rfl },
cases c,
repeat { exact rfl },
end
theorem R.mul_comm (a b : R): a * b = b * a :=
begin
cases a,
cases b,
repeat { exact rfl },
cases b,
repeat { exact rfl },
end
theorem R.eq_zero_or_eq_zero_of_mul_eq_zero (a b : R) (h: a * b = 0): a = 0 ∨ b = 0:=
begin
cases a,
cases b,
left,
exact rfl,
left,
exact rfl,
cases b,
right,
exact rfl,
exfalso,
finish,
end
instance ex7a_kyle_miller : integral_domain R :=
{
zero := R.zero,
one := R.one,
add := R.add,
mul := R.mul,
add_assoc := R.add_assoc,
zero_add := R.zero_add,
add_zero := R.add_zero,
neg := R.neg,
add_left_neg := R.add_left_neg,
add_comm := R.add_comm,
one_mul := R.one_mul,
mul_assoc := R.mul_assoc,
mul_one := R.mul_one ,
left_distrib := R.left_distrib,
right_distrib := R.right_distrib,
mul_comm := R.mul_comm,
exists_pair_ne := R.exists_pair_ne,
eq_zero_or_eq_zero_of_mul_eq_zero := R.eq_zero_or_eq_zero_of_mul_eq_zero,
}
```

#### Yakov Pechersky (Jan 21 2021 at 23:33):

`exact rfl`

can also be `refl`

#### Yakov Pechersky (Jan 21 2021 at 23:34):

If you have a tactic you're applying `repeat`

edly to complete, you can use the semicolon `;`

like so:

```
theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
cases a;
cases b;
cases c;
refl
end
```

#### Yakov Pechersky (Jan 21 2021 at 23:34):

"For each a, for each b, for each c, refl".

#### Lars Ericson (Jan 21 2021 at 23:38):

Thanks Yakov!

The last one `R.eq_zero_or_eq_zero_of_mul_eq_zero`

didn't follow as much of a pattern as the others.

#### Yakov Pechersky (Jan 21 2021 at 23:59):

```
theorem R.eq_zero_or_eq_zero_of_mul_eq_zero (a b : R) (h: a * b = 0): a = 0 ∨ b = 0:=
begin
have h0 : 0 = zero := rfl,
have h1 : 1 = one := rfl,
rw h0 at *,
have : one * one ≠ zero,
{ rw [←h1, R.one_mul, h1],
simp },
cases a;
cases b;
simpa [h] using this <|> simp
end
```

#### Lars Ericson (Jan 22 2021 at 00:20):

There is also an exercise 7b:

Screenshot-from-2021-01-21-19-14-03.png

I give this a passing grade:

```
import ring_theory.subring
import tactic
import tactic.slim_check
import data.zmod.basic
inductive R
| zero
open R
def R.add : R → R → R
| zero zero := zero
def R.mul : R → R → R
| zero zero := zero
def R.neg : R → R
| zero := zero
instance : has_add R := ⟨R.add⟩
instance : has_mul R := ⟨R.mul⟩
instance : has_zero R := ⟨zero⟩
instance : has_neg R := ⟨R.neg⟩
theorem R.not_exists_pair_ne : ¬ ∃ (x y : R), x ≠ y :=
begin
intro h,
cases h with a ha,
cases ha with b hb,
cases a,
cases b,
finish,
end
```

#### Lars Ericson (Jan 22 2021 at 00:25):

There is also a related 8A:

Screenshot-from-2021-01-21-19-21-37.png

I guess what they are asking is to prove that, if R has every property (including having 1 and the other properties above that involve 1) except 0 not equal to 1, then you can prove that R={0}. I'm not sure quite how to set that up in Lean, because among other things it requires that, other than providing 0 and 1, there may be any number of other elements in R, and then we have to prove that the only element in R is 0.

Which I guess gives me a way of expressing it in Lean: Assuming all properties hold and there are no two different elements, then every element must be the 0 element. Except that you can't even state the other properties that are not claimed to be missing, namely

```
--one := R.one,
--one_mul := R.one_mul,
--mul_one := R.mul_one ,
--exists_pair_ne := R.exists_pair_ne,
```

These can't be expressed at all, except if we assume that `one`

is a synonym for `zero`

. In terms of inductive structure definitions, I don't know how to make that claim, so I guess I have to declare an additional constant after declaring the structure.

#### Kyle Miller (Jan 22 2021 at 08:23):

Maybe this is a setup for the Lean version of these problems (using `unit`

as a convenient singleton type):

```
import algebra.ring
import data.equiv.ring
universes u
def eq_zero_or_eq_zero_of_mul_eq_zero' (α : Type u) [ring α] : Prop :=
∀ a b : α, a * b = 0 → a = 0 ∨ b = 0
def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0
instance : comm_ring unit :=
{ zero := (),
one := (),
add := λ _ _, (),
mul := λ _ _, (),
neg := λ _, (),
add_assoc := by { intros, refl },
add_comm := by { intros, refl },
zero_add := by { rintro ⟨_⟩, refl },
add_zero := by { rintro ⟨_⟩, refl },
add_left_neg := by { rintro ⟨_⟩, refl },
mul_assoc := by { intros, refl },
mul_comm := by { intros, refl },
one_mul := by { rintro ⟨_⟩, refl },
mul_one := by { rintro ⟨_⟩, refl },
left_distrib := by {intros, refl },
right_distrib := by {intros, refl } }
lemma prob_7b : eq_zero_or_eq_zero_of_mul_eq_zero' unit :=
sorry
lemma prob_7b' : ¬nontrivial unit :=
sorry
lemma punit_is_zero_ring : is_zero_ring unit :=
sorry
/-- Every zero ring is isomorphic to the above ring. -/
def zero_ring_iso_punit (α : Type u) [ring α] (h : is_zero_ring α) :
α ≃+* unit :=
{ to_fun := λ _, 0,
inv_fun := λ _, 0,
left_inv := λ x, (h x).symm,
right_inv := by { rintro ⟨_⟩, refl },
map_add' := by { intros, refl, },
map_mul' := by { intros, refl, } }
lemma prob_8a (S : Type u) [comm_ring S]
(h₁ : eq_zero_or_eq_zero_of_mul_eq_zero' S) (h₂ : ¬is_zero_ring S) :
integral_domain S :=
sorry
```

#### Eric Wieser (Jan 22 2021 at 08:58):

Mathlib already has `comm_ring unit`

as docs#punit.comm_ring

#### Lars Ericson (Jan 22 2021 at 14:06):

Thanks for these sketches. Please correct me if I'm wrong, but they both give an explicit carrier set.

I'm trying to wrap my head around the idea of showing that, if I have an arbitrary set of something arbitrary, and it has all the properties of `integral_domain`

except `eq_zero_or_eq_zero_of_mul_eq_zero`

, then the carrier set must be `{0}`

. On paper it's elementary. Stating exactly that in exactly that way I'm not sure how to do in Lean, i.e., without constructing the set except to just set that it is `set A`

for `A: Type*`

. The problem with `set A`

is that I then need to establish things like `has_mem`

for `A`

and I don't have those things, so it gets complicated.

#### Eric Wieser (Jan 22 2021 at 15:08):

Did you mean all properties of integral_domain except `exists_pair_ne`

?

#### Eric Wieser (Jan 22 2021 at 15:10):

I think your theorem statement is:

```
import data.equiv.ring
import algebra.punit_instances
example {A : Type*} [comm_ring A] [no_zero_divisors A] (h : (0 : A) = 1) : A ≃+* unit := sorry
```

#### Eric Wieser (Jan 22 2021 at 15:11):

Which reads, if a ring has no zero divisors but has 0 = 1, then it must be isomorphic to the zero ring

#### Eric Wieser (Jan 22 2021 at 15:19):

The only interesting part of the proof is docs#subsingleton_of_zero_eq_one

#### Eric Wieser (Jan 22 2021 at 15:22):

I was hoping we had this, but we don't:

```
example {S R : Type*} [subsingleton S] [subsingleton R] [nonempty S] [nonempty R] : R ≃ S := by library_search
-- fails
```

#### Mario Carneiro (Jan 22 2021 at 16:33):

It needs `inhabited`

#### Eric Wieser (Jan 22 2021 at 16:36):

Even then, I can't find it. Is it missing, or am I just missing an import?

```
example {S R : Type*} [subsingleton S] [subsingleton R] [inhabited S] [inhabited R] : R ≃ S :=
{ to_fun := default _,
inv_fun := default _,
left_inv := λ _, subsingleton.elim _ _,
right_inv := λ _, subsingleton.elim _ _}
```

#### Mario Carneiro (Jan 22 2021 at 16:50):

there might be a theorem saying that subsingleton + inhabited = unique, and an equiv between uniques

#### Kyle Miller (Jan 22 2021 at 19:05):

Lars Ericson said:

I'm trying to wrap my head around the idea of showing that, if I have an arbitrary set of something arbitrary, and it has all the properties of

`integral_domain`

except`eq_zero_or_eq_zero_of_mul_eq_zero`

, then the carrier set must be`{0}`

.

The only point of bringing in `unit`

as a ring was to say that if every element equaled `0`

(i.e., its carrier set is zero), then the ring is isomorphic to `unit`

(see `zero_ring_iso_punit`

) and hence the original ring has the structure described by the problem. You could also prove that if there is an isomorphism, then every element equals `0`

. You don't really need to talk about the carrier set itself, since the `is_zero_ring`

predicate captures the notion.

But if for some reason you want to talk about carrier sets, you can use `set.univ`

:

```
lemma zero_ring_carrier_eq_zero (α : Type u) [ring α] :
is_zero_ring α ↔ (set.univ : set α) = {0} :=
begin
split,
{ intro h, ext x, simp [h x], },
{ intros h x,
have h' := set.mem_univ x,
rw h at h',
simpa using h', },
end
```

#### Lars Ericson (Jan 23 2021 at 18:45):

I'm trying to understand this. What your definition gives:

```
def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0
lemma zero_ring_carrier_eq_zero (α : Type u) [ring α] :
is_zero_ring α ↔ (set.univ : set α) = {0} :=
begin
split,
{ intro h, ext x, simp [h x], },
{ intros h x,
have h' := set.mem_univ x,
rw h at h',
simpa using h', },
end
```

is a way of transferring a proof that every element of a type is 0 into a proof that every element of a set of that type equals 0. So it's a technical conversion of type equals `{0}`

to set of type equals `{0}`

.

What the exercise calls for is to prove that if I have a type `R`

which is assumed to have all of the `integral_domain`

properties but `exists_pair_ne`

, then `R={0}`

. The setup for this may or may not involve `zero_ring_carrier_eq_zero`

to transfer from type argument to a set argument.

I think exercise 8A is the converse of 7B. 7B says "`{0} → `

an integral domain except for `exists_pair_ne`

". 8A says that " `R`

is almost an integral domain except for `exists_pair_ne → R={0}`

:

Screenshot-from-2021-01-23-13-42-54.png

#### Lars Ericson (Jan 23 2021 at 18:48):

Most importantly, the contents of `R`

are not specified in advance as ` ∀ (x : α), x = 0`

. The contents of `R`

are implicitly specified, without being constructed, by satisfying all of the `integral_domain`

properties except `exists_pair_ne`

. So there is no concrete specification of the type, inductive or otherwise. Only implicit specification through the properties.

#### Kyle Miller (Jan 23 2021 at 19:12):

I'm not familiar with what book you're following, but presumably it's in terms of set theory. Lean is based in type theory, and it usually takes a bit of translation to get the right idioms. What I was trying to say is "a way to write $S=\{0\}$ in type theory is `is_zero_ring S`

, and if that's not convincing, then `zero_ring_carrier_eq_zero`

shows that `S`

as a set is indeed `{0}`

(where `0 : S`

is the zero element of type `S`

that `ring S`

gives). This last piece of code is not meant to answer the full exercise -- it's just conceptual for sets vs types -- and it doesn't replace the `prob_*`

lemmas from my earlier comment.

#### Kyle Miller (Jan 23 2021 at 19:16):

@Eric Wieser had another translation, too. Both of ours are using that $p \to (q \vee r)$ is $p \to \neg r \to q$ (but we chose a different thing to negate, basically) since the latter form can be more convenient, at least for the theorem statement and proof.

#### Kyle Miller (Jan 23 2021 at 19:19):

(I did this conversion because `integral_domain S`

is not a `Prop`

, so you can't $\vee$ it with `is_zero_ring S`

. One way to say something "is" an integral domain is to give a full `integral_domain S`

structure. This isn't exactly the best idea, though, since it doesn't guarantee that this structure has anything to do with the original ring structure on S...)

#### Lars Ericson (Jan 23 2021 at 19:22):

Thanks. The book is A survey of modern algebra, 4th edition, by Garret Birkhoff and Saunders Mac Lane. I am trying to start by specifying the list of properties assumed to hold. One problem is that with an abstract type R and hence no definition of 0, 1, `plus`

and `mul`

, I don't have the syntax to state the properties. I got this far:

```
import ring_theory.subring
import tactic
import tactic.slim_check
variable R: Type*
variable R.add : R → R → R
variable R.mul : R → R → R
variable R.neg : R → R
variable R.zero : R
variable R.one : R
theorem R.zero_add (a : R) (zero: R): zero + a = a := sorry
```

but I get errors of form

```
failed to synthesize type class instance for
R : Type u_1,
a zero : R
⊢ has_add R
```

#### Lars Ericson (Jan 23 2021 at 19:24):

I want to just say I have some `R`

and it has these operations like `mul : R → R → R`

and they have these properties:

```
variable R: Type*
variable R.add : R → R → R
variable R.mul : R → R → R
variable R.neg : R → R
variable R.zero : R
variable R.one : R
theorem R.zero_add (a : R) (zero: R): zero + a = a
theorem R.add_zero (a : R): a + 0 = a
theorem R.add_assoc (a b c : R): a + b + c = a + (b + c)
theorem R.add_left_neg (a : R): -a + a = 0
theorem R.add_comm (a b : R): a + b = b + a
theorem R.mul_assoc (a b c : R): a * b * c = a * (b * c)
theorem R.left_distrib (a b c : R): a * (b + c) = a * b + a * c
theorem R.right_distrib (a b c : R): (a + b) * c = a * c + b * c
theorem R.mul_comm (a b : R): a * b = b * a
theorem R.eq_zero_or_eq_zero_of_mul_eq_zero (a b : R) (h: a * b = 0): a = 0 ∨ b = 0
theorem R.one_mul (a : R): 1 * a = a
theorem R.mul_one (a : R): a * 1 = a
theorem R.not_exists_pair_ne : ¬ ∃ (x y : R), x ≠ y
```

and the only solution `R`

for the logical system of equations consisting of that set of properties is `{0}`

.

#### Kyle Miller (Jan 23 2021 at 19:26):

The idea of typeclasses is that they associate operations and axioms to a type. `(α : Type u) [comm_ring α]`

gives you most of those, except `eq_zero_or_eq_zero_of_mul_eq_zero`

and `not_exists_pair_ne`

#### Kyle Miller (Jan 23 2021 at 19:27):

and it's not specifying anything about `α`

itself (in the sense of inductive definitions)

#### Lars Ericson (Jan 23 2021 at 19:28):

Thanks I will look at the source for `comm_ring`

. Without relying on the hierarchy that is already in lean, I want to make a similar thing called `almost_integral_domain_without_exists_pair_ne`

.

#### Kyle Miller (Jan 23 2021 at 19:29):

(typeclasses are how we implement "abuse of notation," also known as synecdoche: the `α`

stands in for the commutative ring structure itself because Lean will locate the relevant typeclass instance, which is the commutative ring structure for the type.)

#### Kyle Miller (Jan 23 2021 at 19:30):

All an `integral_domain`

is really is a `comm_ring`

with these two additional axioms, so you can work with `comm_ring`

and have these axioms as hypotheses or conclusions in your lemmas/theorems

#### Kyle Miller (Jan 23 2021 at 19:31):

though `not_exists_pair_ne`

is implemented with the `nontrivial`

typeclass

#### Kyle Miller (Jan 23 2021 at 19:34):

For example, this might be another rendering of problem 8(a):

```
lemma prob_8a (S : Type u) [comm_ring S] (h : eq_zero_or_eq_zero_of_mul_eq_zero S) :
is_zero_ring S ∨ not_exists_pair_ne S :=
sorry
```

with the understanding that a `comm_ring`

satisfying both `eq_zero_or_eq_zero_of_mul_eq_zero`

and `not_exists_pair_ne`

*is* an integral domain.

#### Kyle Miller (Jan 23 2021 at 19:37):

Or packaging up some of this, you could say

```
structure is_integral_domain (R : Type u) [comm_ring R] : Prop :=
(not_exists_pair_ne : ¬ ∃ (x y : R), x ≠ y)
(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : R), a * b = 0 → a = 0 ∨ b = 0)
lemma prob_8a (S : Type u) [comm_ring S]
(h : ∀ (a b : R), a * b = 0 → a = 0 ∨ b = 0) :
is_zero_ring S ∨ is_integral_domain S :=
sorry
```

#### Eric Wieser (Jan 23 2021 at 19:38):

`almost_integral_domain_without_...`

is just docs#no_zero_divisors, which is what I use I my solution above

#### Eric Wieser (Jan 23 2021 at 19:40):

Regarding "it's not a prop so you can't or it", you can use `nonempty (integral_domain _)`

to make it a prop

#### Kyle Miller (Jan 23 2021 at 19:42):

Lars Ericson said:

but I get errors of form

`failed to synthesize type class instance for R : Type u_1, a zero : R ⊢ has_add R`

Answering this question, the issue is that you didn't introduce `[has_add R]`

variables -- these are where the `+`

notation comes from.

#### Lars Ericson (Jan 23 2021 at 21:53):

Thanks Kyle and Eric. `is_integral_domain`

already exists, so the package becomes:

```
import ring_theory.subring
import tactic
import tactic.slim_check
import data.equiv.ring
import algebra.punit_instances
universe u
def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0
lemma ex8a_kyle_miller (S : Type u) [comm_ring S]
(h : ∀ (a b : S), a * b = 0 → a = 0 ∨ b = 0) :
is_integral_domain S ∨ is_zero_ring S :=
sorry
lemma ex8a_eric_wieser {S: Type*} [comm_ring S] [no_zero_divisors S] (h : (0 : S) = 1) : S ≃+* unit :=
sorry
```

Kyle's version seems more evocative of the exact phrasing of the problem. The proposition

```
is_integral_domain S ∨ is_zero_ring S
```

directly reflects the problem statement "S is either an integral domain or the system consisting of 0 alone".

I will try to prove both versions. Thanks for the help!

#### Eric Wieser (Jan 23 2021 at 22:04):

Yes, I think Kyle's phrasing more directly matches the question

#### Eric Wieser (Jan 23 2021 at 22:06):

`nonempty (S \equiv+* unit)`

is equivalent to `is_zero_ring S`

, and the translation is uninteresting

#### Kyle Miller (Jan 23 2021 at 22:16):

Eric pointed out `no_zero_divisors`

exists, so you could phrase it as

```
lemma ex8a_kyle_miller (S : Type u) [comm_ring S] [no_zero_divisors S] :
is_integral_domain S ∨ is_zero_ring S :=
sorry
```

This gives hypothesis gives you `eq_zero_or_eq_zero_of_mul_eq_zero`

. (`no_zero_divisors`

is an example of using the typeclass system to provide certain kinds of basic properties of something automatically.)

#### Lars Ericson (Jan 23 2021 at 22:33):

Thanks, I will update `ex8a_kyle_miller`

. For Eric's version I was able to prove it just by using the autopilot features on Lean, without really understanding what it says (for example I've never seen `≃+* `

before):

```
import ring_theory.subring
import tactic
import tactic.slim_check
import data.equiv.ring
import algebra.punit_instances
universe u
def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0
lemma ex8a_eric_wieser {S: Type*} [CR: comm_ring S]
[NZD: no_zero_divisors S] (h : (0 : S) = 1) : S ≃+* unit :=
begin
refine ring_equiv.symm _,
refine {to_fun := _, inv_fun := _, left_inv := _, right_inv := _, map_mul' := _, map_add' := _},
intro h,
exact ring.one,
intro h1,
exact (),
rw function.left_inverse,
intro x,
exact unit.ext,
rw function.right_inverse,
rw function.left_inverse,
intro x,
exact eq_of_zero_eq_one h ring.one x,
intro u1,
intro u2,
ring,
exact eq_of_zero_eq_one h ring.one (ring.one * ring.one),
intro u1,
intro u2,
exact eq_of_zero_eq_one h ring.one (ring.one + ring.one),
end
```

#### Eric Wieser (Jan 23 2021 at 23:12):

Proving Kyle's should be easy after `by_cases h : (0 : R) = 1`

#### Lars Ericson (Jan 23 2021 at 23:14):

Yes, thanks, here it is:

```
import ring_theory.subring
import tactic
import tactic.slim_check
import data.equiv.ring
import algebra.punit_instances
universe u
def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0
lemma ex8a_kyle_miller (S : Type u) [comm_ring S] [no_zero_divisors S] :
is_integral_domain S ∨ is_zero_ring S :=
begin
by_cases h: (1:S) ≠ (0:S),
fconstructor,
refine {exists_pair_ne := _, mul_comm := _, eq_zero_or_eq_zero_of_mul_eq_zero := _},
use [0,1],
refine ne_comm.mp _,
assumption,
exact mul_comm,
exact λ {a b : S}, mul_eq_zero.mp,
refine or.inr _,
rw is_zero_ring,
refine eq_zero_of_zero_eq_one _,
finish,
end
```

#### Lars Ericson (Jan 23 2021 at 23:23):

Exercise 8B is "Is 0≠1 used in proving Rules 1-9?". These rules are as follows, I think the answer is No (these are all provided from the definition of commutative ring):

```
import algebra.ring.basic
universe u
variables {α : Type u} [comm_ring α] {a b c d z x₁ x₂ : α}
lemma rule_1 : (a+b)*c=a*c+b*c := add_mul _ _ _
lemma rule_2_plus : (0 + a = a) := zero_add _
lemma rule_2_times : (1 * a = a) := one_mul _
lemma rule_3 : (∀ (a : α), a + z = a) → z = 0 :=
begin
intro h1,
have h2 := h1 0,
exact add_left_eq_self.mp (congr_arg (has_add.add z) (congr_arg (has_add.add z) (h1 z))),
end
lemma rule_4 : a + b = a + c → b = c := (add_right_inj a).mp
lemma rule_5 : a + x₁ = 0 → a + x₂ = 0 → x₁ = x₂ :=
begin
intro h1,
intro h2,
exact neg_unique h1 h2,
end
lemma rule_6 : a + x₁ = b → a + x₂ = b → x₁ = x₂ :=
begin
intro h1,
intro h2,
rw ← h1 at h2,
exact rule_4 (eq.symm h2),
end
lemma rule_7a : a * 0 = 0 := mul_zero a
lemma rule_7b : 0 * a = 0 := zero_mul a
lemma rule_8 : (∀ (a : α), a*z = a) → z = 1 :=
begin
intro h1,
exact (eq_one_iff_eq_one_of_mul_eq_one (h1 1)).mp rfl,
end
lemma rule_9 : (-a)*(-b) = a*b := neg_mul_neg _ _
```

Last updated: May 11 2021 at 12:15 UTC