zero_mul

Stream: new members

[Iocta]

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]

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]

What's your math proof?

[Kevin Buzzard]

Oh this is a mathematics in Lean question!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

But those are for a comm_ring

[Iocta]

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

[Iocta]

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

[Jalex Stark]

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

[Kevin Buzzard]

Oh well, this is a spoiler :-)

[Reid Barton]

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]

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]

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

[Jalex Stark]

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

[Iocta]

ok i'll try that

[Iocta]

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

[Jalex Stark]

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

[Kevin Buzzard]

You might end up proving mul_zero with that hint :-)

[Jalex Stark]

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]

got it, thanks

[Jalex Stark]

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

[Iocta]

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]

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

[Jalex Stark]

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

[Kevin Buzzard]

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)