Zulip Chat Archive

Stream: new members

Topic: zero_mul


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Reid Barton (May 11 2020 at 19:33):

What's your math proof?

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:33):

Oh this is a mathematics in Lean question!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jalex Stark (May 11 2020 at 19:34):

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

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:34):

But those are for a comm_ring

view this post on Zulip Iocta (May 11 2020 at 19:35):

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

view this post on Zulip Iocta (May 11 2020 at 19:37):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:38):

Oh well, this is a spoiler :-)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Jalex Stark (May 11 2020 at 19:38):

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

view this post on Zulip Jalex Stark (May 11 2020 at 19:39):

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

view this post on Zulip Iocta (May 11 2020 at 19:39):

ok i'll try that

view this post on Zulip Iocta (May 11 2020 at 20:12):

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

view this post on Zulip Jalex Stark (May 11 2020 at 20:46):

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

view this post on Zulip Kevin Buzzard (May 11 2020 at 22:33):

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

view this post on Zulip 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

view this post on Zulip Iocta (May 11 2020 at 23:33):

got it, thanks

view this post on Zulip Jalex Stark (May 11 2020 at 23:58):

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

view this post on Zulip 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

view this post on Zulip Iocta (May 12 2020 at 00:25):

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

view this post on Zulip Jalex Stark (May 12 2020 at 00:26):

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

view this post on Zulip 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