## 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_comm (a * a) (-a * a),
have h: (-a * a) + (a * a) = -(a * a) + (a * a),
from sorry,
rw h,
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)


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

https://github.com/leanprover-community/mathematics_in_lean/blob/0da899df6064a7eb50a7fd49618047d3a3a35963/examples/basic_skills/unnamed_711.lean#L6

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

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

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,
{
},
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