## 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
{"ft_lang_label":"__label__en","ft_lang_prob":0.87913924,"math_prob":0.74067205,"size":3899,"snap":"2021-21-2021-25","text_gpt3_token_len":1360,"char_repetition_ratio":0.17227215,"word_repetition_ratio":0.14126395,"special_character_ratio":0.3998461,"punctuation_ratio":0.1627385,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99551547,"pos_list":[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46],"im_url_duplicate_count":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-05-16T09:43:55Z\",\"WARC-Record-ID\":\"<urn:uuid:7709cd06-7684-41c7-9dc9-637247858b96>\",\"Content-Length\":\"29241\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:ed367fde-f07d-4897-97fe-3b8b2ea0dade>\",\"WARC-Concurrent-To\":\"<urn:uuid:c81240a4-745f-4ae8-93ee-5d5e8dbc1f27>\",\"WARC-IP-Address\":\"185.199.108.153\",\"WARC-Target-URI\":\"https://leanprover-community.github.io/archive/stream/113489-new-members/topic/zero_mul.html\",\"WARC-Payload-Digest\":\"sha1:W7SBZUW6W5BMCQEAEDW46E5BWGXUDB7Q\",\"WARC-Block-Digest\":\"sha1:YSPN75DHNG64Z4XSDW54OKRTWLP2NYVB\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-21/CC-MAIN-2021-21_segments_1620243992516.56_warc_CC-MAIN-20210516075201-20210516105201-00284.warc.gz\"}"}