# Zulip Chat Archive

## Stream: new members

### Topic: zero_mul

#### Iocta (May 11 2020 at 19:31):

```
variables {R : Type*} [ring R]
theorem zero_mul (a : R) : 0 * a = 0 :=
begin
rw ← add_left_neg a,
rw add_mul,
rw add_comm,
rw add_left_neg a,
rw add_comm (a * a) (-a * a),
have h: (-a * a) + (a * a) = -(a * a) + (a * a),
from sorry,
rw h,
rw add_left_neg (a * a),
end
```

#### Iocta (May 11 2020 at 19:32):

*Mathematics in Lean* provides

```
variables (R : Type*) [comm_ring R]
#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (add_left_neg : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)
```

#### Reid Barton (May 11 2020 at 19:33):

What's your math proof?

#### Kevin Buzzard (May 11 2020 at 19:33):

Oh this is a mathematics in Lean question!

#### Kevin Buzzard (May 11 2020 at 19:33):

But is R a ring or a comm_ring? I still don't understand at all what you are asking.

#### Kevin Buzzard (May 11 2020 at 19:34):

```
import tactic
variables {R : Type*} [ring R]
theorem zero_mul' (a : R) : 0 * a = 0 := ring.zero_mul a
```

I'm assuming that this is not the answer.

#### Jalex Stark (May 11 2020 at 19:34):

I think they want a proof using only the ring axioms in their second post

#### Kevin Buzzard (May 11 2020 at 19:34):

But those are for a comm_ring

#### Iocta (May 11 2020 at 19:35):

#### Iocta (May 11 2020 at 19:37):

Let's say we can't assume multiplication is commutative

#### Jalex Stark (May 11 2020 at 19:38):

I second @Reid Barton's question, do you know how to prove this on pen and paper?

#### Kevin Buzzard (May 11 2020 at 19:38):

Oh well, this is a spoiler :-)

#### Reid Barton (May 11 2020 at 19:38):

I don't know what the book wants you to do, but for puzzles like this it's usually easier to work out a proof on paper first

#### Jalex Stark (May 11 2020 at 19:38):

If not, I think the right answer is "think about it for five minutes, and if you can't do it, come back for a hint"

#### Jalex Stark (May 11 2020 at 19:38):

because you probably want to be able to actually solve puzzles like this!

#### Jalex Stark (May 11 2020 at 19:39):

otherwise you wouldn't be reading a book about doing mathematics

#### Iocta (May 11 2020 at 19:39):

ok i'll try that

#### Iocta (May 11 2020 at 20:12):

I keep ending up in a circle. Need a hint.

#### Jalex Stark (May 11 2020 at 20:46):

Hint: think about the equation `b * (a + 0) = b * a`

#### Kevin Buzzard (May 11 2020 at 22:33):

You might end up proving `mul_zero`

with that hint :-)

#### Jalex Stark (May 11 2020 at 22:34):

Ah, true, though it should then be pretty easy to use the same technique to prove `zero_mul`

. I'll leave the hint as-is

#### Iocta (May 11 2020 at 23:33):

got it, thanks

#### Jalex Stark (May 11 2020 at 23:58):

don't leave us hanging, post your Lean code!

#### Iocta (May 12 2020 at 00:24):

turns out the book proves `mul_zero`

, and it's easy to adapt.

```
theorem zero_mul (a : R) : 0 * a = 0 :=
begin
have h : 0 * a + 0 * a = 0 + 0 * a,
{
rw ← add_mul,
rw zero_add,
rw zero_add,
},
rw add_right_cancel h
end
```

#### Iocta (May 12 2020 at 00:25):

not sure I woulda come up with that indirection but that's progress anyway

#### Jalex Stark (May 12 2020 at 00:26):

learning new such "indirections" is one of the fun parts of learning math

#### Kevin Buzzard (May 12 2020 at 06:10):

This is just a "standard trick" if you like. It's of no use in practice because mathematicians are very fluid about their axioms for a ring; you'd probably find that some said this was an axiom anyway (we care far more about confluent rewriting systems than what the axioms of a ring actually *are*)

Last updated: May 16 2021 at 05:21 UTC