# Zulip Chat Archive

## Stream: new members

### Topic: the complex number game

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

Have you done the natural number game? Can you prove complex conjugation is a ring homomorphism?

Link to Lean web editor (takes a long time to load, honestly I'd leave it on "lean is busy" for at least 1 minute before concluding something is wrong):

https://tinyurl.com/thecomplexnumbergame

Source (cut and paste this into any Lean project which uses mathlib and you won't have to wait 1 minute)

This is part of a book I'm writing with Jeremy, Rob and Patrick. All comments from mathematicians welcome!

#### Aniruddh Agarwal (May 10 2020 at 12:23):

```
structure complex : Type :=
(re : ℝ) (im : ℝ)
```

Is the code above roughly equivalent to the Haskell:

```
data Complex = C Real Real
```

#### Patrick Stevens (May 10 2020 at 12:34):

Aniruddh Agarwal said:

`structure complex : Type := (re : ℝ) (im : ℝ)`

Is the code above roughly equivalent to the Haskell:

`data Complex = C Real Real`

Basically, but the fields are named in Lean whereas you haven't named them in the Haskell.

#### Kevin Buzzard (May 20 2020 at 21:32):

I'm trying to work out a path to building a basic mathematical API for the complexes in a way that a mathematician can understand easily. I've got something which I think works ok and I'll be live streaming a walkthrough of a basic complex number game on twitch tomorrow Thursday 21st 5pm UK time.

#### Jalex Stark (May 21 2020 at 00:10):

(If you "follow" kevin at https://www.twitch.tv/kbuzzard, you'll get an email when he goes live)

#### Johan Commelin (May 21 2020 at 03:53):

walkthrough or speedrun?

#### Kevin Buzzard (May 21 2020 at 07:18):

Walkthrough

#### Kevin Buzzard (May 21 2020 at 07:18):

Basically I have got what I think is a really nice proof that C is a ring which hopefully will convince people that lean is easy

#### Kevin Buzzard (May 21 2020 at 07:19):

And by the time they're using it and realise that it's hard, it's too late they're hooked

#### Kenny Lau (May 21 2020 at 07:20):

what, `by ring`

?

#### Kevin Buzzard (May 21 2020 at 07:21):

It's my_complex

#### Kevin Buzzard (May 21 2020 at 15:50):

https://github.com/ImperialCollegeLondon/complex-number-game

#### Patrick Massot (May 21 2020 at 15:53):

Do you want this to be added to https://leanprover-community.github.io/learn.html or is this a transient thing waiting to be integrated to MIL?

#### Patrick Massot (May 21 2020 at 15:54):

Yes you'd like this to be added, then you simply need to click the edit button at https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/learn.md to open a PR

#### Kevin Buzzard (May 21 2020 at 17:14):

This was just a gimmick. I am happy to use it any way you think is best.

#### Filippo A. E. Nuccio (May 22 2020 at 18:11):

I can't understand the lines

```
def Conj : ℂ →+* ℂ :=
{ to_fun := conj,
map_one' := begin ext; simp, end,
map_mul' := begin intros, ext; simp end,
map_zero' := begin ext; simp end,
map_add' := begin intros, ext; simp end}
```

in the Complex Numbers Game,

#### Kevin Buzzard (May 22 2020 at 18:12):

Did you understand the question? That looks like the solution

#### Filippo A. E. Nuccio (May 22 2020 at 18:12):

No, indeed (as you said yesterday), I guess I don't know what an equivalence relation is.

#### Filippo A. E. Nuccio (May 22 2020 at 18:12):

I understand that conj could take (x,y) and send it to (x,-y)

#### Kevin Buzzard (May 22 2020 at 18:13):

The question is probably the same as the solution except that between each `begin end`

block there is a `sorry`

#### Filippo A. E. Nuccio (May 22 2020 at 18:13):

and solved all the exercises related to conj.

#### Kevin Buzzard (May 22 2020 at 18:13):

and if you click on the `sorry`

you will see the goal which Lean wants you to prove.

#### Filippo A. E. Nuccio (May 22 2020 at 18:14):

I suspect I don't know what it means to " define a function" (more than specifying where it should send every element of the domain)

#### Kevin Buzzard (May 22 2020 at 18:14):

I don't know what you are talking about. What function?

#### Kevin Buzzard (May 22 2020 at 18:14):

This is the question:

```
/-- the ring homomorphism complex conjugation -/
def Conj : ℂ →+* ℂ :=
{ to_fun := conj,
map_zero' := begin sorry end,
map_one' := begin sorry end,
map_add' := begin sorry end,
map_mul' := begin sorry end
}
```

#### Kevin Buzzard (May 22 2020 at 18:15):

I have done the hard work (the computer science stuff).

#### Filippo A. E. Nuccio (May 22 2020 at 18:15):

you begin with

`def Conj : C->+* C :=`

#### Kevin Buzzard (May 22 2020 at 18:15):

Yes but you don't need to worry about all that part

#### Kevin Buzzard (May 22 2020 at 18:15):

Sorry, what is your question?

#### Kevin Buzzard (May 22 2020 at 18:15):

Did you manage to fill in the `sorry`

s yourself?

#### Filippo A. E. Nuccio (May 22 2020 at 18:16):

Indeed, I haven't realised I could click on the sorry to understand what Lean wanted from me

#### Filippo A. E. Nuccio (May 22 2020 at 18:16):

I agree that now everything looks trivial (or at the same level of previous exercices), so no problem. An thanks.

#### Filippo A. E. Nuccio (May 22 2020 at 18:16):

But still one small point eludes me:

#### Kevin Buzzard (May 22 2020 at 18:17):

OK so the question for mathematicians is supposed to be the following: "replace each `sorry`

with a tactic proof. You can see what the goal is in each case by clicking on the `sorry`

"

#### Filippo A. E. Nuccio (May 22 2020 at 18:17):

What is the point of these lines? I gather that it is to state the lemma "the set-theoretic map conj is actually a ring homomoprhism", is that right?

#### Kevin Buzzard (May 22 2020 at 18:17):

I only released the game yesterday and I didn't try it out on some select group of people or anything -- I am sure that there will be plenty of things that need to be clarified.

#### Kevin Buzzard (May 22 2020 at 18:17):

Yes, so that's the other question we have here.

#### Kevin Buzzard (May 22 2020 at 18:18):

You might know that to define a complex number `z`

in Lean we could do something like `{ re := 3, im := 4}`

#### Filippo A. E. Nuccio (May 22 2020 at 18:18):

Yes

#### Kevin Buzzard (May 22 2020 at 18:18):

Well, to define a ring homomorphism from $\mathbb{C}$ to $\mathbb{C}$ it's the same kind of story

#### Kevin Buzzard (May 22 2020 at 18:18):

We need to give Lean a map, and four proofs

#### Filippo A. E. Nuccio (May 22 2020 at 18:18):

I believe that my problem is that those lines begin with `def`

rather than `lemma`

#### Kevin Buzzard (May 22 2020 at 18:19):

`def z := { re := 3, im := 4}`

also has a `def`

#### Kevin Buzzard (May 22 2020 at 18:19):

as does `def conj (z : ℂ) : ℂ := sorry`

#### Kevin Buzzard (May 22 2020 at 18:20):

If you are defining things, you use `def`

or `definition`

. If you are proving theorems you use `theorem`

or `lemma`

#### Filippo A. E. Nuccio (May 22 2020 at 18:20):

This line (435 in the code) is OK with me: it defines a function taking a complex number to another complex number.

#### Kevin Buzzard (May 22 2020 at 18:21):

We are defining the ring homomorphism, and part of the definition is the underlying function. We are *not* proving that a function is a ring homomorphism, we are defining a ring homomorphism to be a collection of data, most of which is proofs, but not all of it, so we use `def`

#### Filippo A. E. Nuccio (May 22 2020 at 18:21):

What puzzles me are the line where you check it is a ring hom: they begin with

`def Conj : ℂ →+* ℂ :=`

#### Kevin Buzzard (May 22 2020 at 18:21):

I am defining a second thing

#### Kevin Buzzard (May 22 2020 at 18:21):

`conj`

is the function, `Conj`

is the ring homomorphism

#### Filippo A. E. Nuccio (May 22 2020 at 18:21):

(the invisible map again is in the background, I suspect)

#### Kevin Buzzard (May 22 2020 at 18:22):

There's an invisible map from ring homs to functions, and it will send Conj to conj.

#### Kevin Buzzard (May 22 2020 at 18:22):

`Conj`

is a variable that contains a lot of data, including `conj`

#### Filippo A. E. Nuccio (May 22 2020 at 18:23):

Ahah! Clear: so, I am correct in saying that

1) the to_fun line says that the underlying function to Conj is conj

2) the ->+* is telling Lean that we are going to define a ring hom

3) the map_one' until map_add' are the axioms a ring hom must satisfy (because we told him already that a ring hom is by definition something which satisfies them)

#### Kevin Buzzard (May 22 2020 at 18:25):

Mathematicians think that `Conj`

and `conj`

are equal, because to a mathematician the "object" is just the function, and the proofs of the axioms are not things you can make with sets -- the proofs live in some other part of the story.

In Lean, proofs are objects, just like functions are, so you can make objects which package together functions and proofs. `conj`

has no packaging -- it's just the function. `Conj`

is the package: the function, and the proofs, all in one object. In type theory, proofs are no different to numbers -- they are just terms, which can be packaged together.

#### Filippo A. E. Nuccio (May 22 2020 at 18:26):

Wonderful, it does make sense. In particular, I guess that before a mathematician (or myself, at least) can do something cool with Lean, this part of the story needs to be fully digested.

#### Filippo A. E. Nuccio (May 22 2020 at 18:27):

But it seems very edible.

#### Kevin Buzzard (May 22 2020 at 18:27):

Do you have `leanproject`

installed @Filippo A. E. Nuccio ? If you do then there is now a much easier way to play the complex number game: you can just download and compile the repository with `leanproject get ImperialCollegeLondon/complex-number-game`

#### Filippo A. E. Nuccio (May 22 2020 at 18:27):

Yes, I have already done so.

#### Kevin Buzzard (May 22 2020 at 18:27):

and then you can solve the levels individually in VS Code

#### Filippo A. E. Nuccio (May 22 2020 at 18:27):

I am playing on my pc, actually

#### Kevin Buzzard (May 22 2020 at 18:27):

I asked because you mentioned line 435

#### Kevin Buzzard (May 22 2020 at 18:28):

but I have pulled everything off into individual chapters now, in their own files, e.g. https://github.com/ImperialCollegeLondon/complex-number-game/blob/master/src/complex/conj.lean

#### Filippo A. E. Nuccio (May 22 2020 at 18:28):

That was from the github page, because I feared I could not make myself clear.

#### Kevin Buzzard (May 22 2020 at 18:29):

I don't think any file in the github repo I'm talking about has as many as 435 lines.

#### Filippo A. E. Nuccio (May 22 2020 at 18:29):

https://github.com/kbuzzard/xena/blob/master/Mathematics_In_Lean_ideas/complex_solns.lean

#### Kevin Buzzard (May 22 2020 at 18:30):

Right. What I'm trying to say is that I have made a more sophisticated version of this game now

#### Filippo A. E. Nuccio (May 22 2020 at 18:31):

Now I got it, thanks; sorry for not grasping it more quickly.

#### Kevin Buzzard (May 22 2020 at 18:31):

https://www.twitch.tv/videos/627659597 if you want to see me playing through the tutorial level

#### Filippo A. E. Nuccio (May 22 2020 at 18:31):

I attended it live, actually .

#### Kevin Buzzard (May 22 2020 at 18:31):

and on Thursday 21st I'll be solving `I`

and `conj`

live

#### Filippo A. E. Nuccio (May 22 2020 at 18:32):

You mean that yesterday you'll be solving them?

#### Kevin Buzzard (May 22 2020 at 18:32):

oops Thursday 28th :-)

#### Patrick Massot (May 22 2020 at 18:32):

Kevin, that's what you get for encouraging people to be rigorous

#### Filippo A. E. Nuccio (May 22 2020 at 18:33):

I hope to be done with the full proof that C is a field by next week, as I would like to move towards factorizing ideals as products of primes in Dedekind domains.

#### Filippo A. E. Nuccio (May 22 2020 at 18:34):

Thank you for your help, in the meantime.

#### Kevin Buzzard (May 22 2020 at 18:34):

I don't give any hints for this, and it's slightly tricky to get started. You should be warned that Lean's axioms for a field are not what we usually teach!

#### Kevin Buzzard (May 22 2020 at 18:35):

Check this out: a field is a nonzero commutative ring equipped with a map `inv : K -> K`

satisfying `inv(0)=0`

, and `x*inv(x)=1`

if `x`

isn't `0`

#### Kevin Buzzard (May 22 2020 at 18:36):

I'm sure you can see that this is trivially equivalent to what we think a field is

#### Filippo A. E. Nuccio (May 22 2020 at 18:36):

Sure

#### Kevin Buzzard (May 22 2020 at 18:36):

But they like their functions to be defined everywhere for technical reasons to do with implementation issues

#### Kevin Buzzard (May 22 2020 at 18:37):

Note that `a/b`

is defined to be `a*inv(b)`

, so in particular `1/0=0`

#### Filippo A. E. Nuccio (May 22 2020 at 18:37):

(are "they" computer scientists?)

#### Kevin Buzzard (May 22 2020 at 18:37):

This means that you can define `inv(z)`

to be `{re := re(z)/norm_sq(z), im := -im(z)/norm_sq(z)}`

#### Filippo A. E. Nuccio (May 22 2020 at 18:38):

Sure, this makes sense.

#### Kevin Buzzard (May 22 2020 at 18:38):

and if `z=0`

this will give you 0, which is what the CS people want

#### Filippo A. E. Nuccio (May 22 2020 at 18:38):

Great. It all makes sense, and also explains why norms come before it being a field.

#### Patrick Massot (May 22 2020 at 18:39):

Filippo A. E. Nuccio said:

I hope to be done with the full proof that C is a field by next week, as I would like to move towards factorizing ideals as products of primes in Dedekind domains.

I love that sentence.

#### Patrick Massot (May 22 2020 at 18:39):

I wish our students could be that ambitious.

#### Kevin Buzzard (May 22 2020 at 18:40):

I intentionally put the proof it was a ring before the definition of $i$, because as a mathematician I feel like $i$ is the first thing you want to define, and I thought it really interesting that you can prove $\mathbb{C}$ is a ring without ever mentioning it explicitly.

#### Patrick Massot (May 22 2020 at 18:42):

And I also wish people could stop teaching set theory bullshit to our students. I'm marking exams and I just saw. Let's fix $(f, g) \in \left(\mathbb R^{\mathbb R}\right)^2$ instead of $f, g : \mathbb R \to \mathbb R$...

#### Kevin Buzzard (May 22 2020 at 18:42):

It's defeq Patrick so you can't take a mark off

#### Filippo A. E. Nuccio (May 22 2020 at 18:42):

That's terrifying, though...

#### Kevin Buzzard (May 22 2020 at 18:43):

That's the French for you

#### Patrick Massot (May 22 2020 at 18:44):

And those are my students who used Lean for 12 weeks...

#### Filippo A. E. Nuccio (May 22 2020 at 18:46):

Patrick Massot said:

And those are my students who used Lean for 12 weeks...

BTW: I might ask you hints on how to teach Lean to my students as well, also in France (Saint-Étienne), but this will come later. I might need to first lea(r)n it myself.

#### Patrick Massot (May 22 2020 at 18:47):

Did you do the tutorials based on my course?

#### Filippo A. E. Nuccio (May 22 2020 at 18:51):

Some of them, yes. Almost all of them, actually.

#### Patrick Massot (May 22 2020 at 18:55):

You can also get the French version on my web page (together with the lecture notes and tactic cheat sheet).

#### Kevin Buzzard (May 22 2020 at 19:18):

@Filippo A. E. Nuccio I just pushed solutions to `field.lean`

in the complex number game repo

#### Filippo A. E. Nuccio (May 22 2020 at 19:34):

Thanks to both of you!

#### Patrick Massot (May 22 2020 at 19:42):

Actually if you are interested in the French version then I'll do some cleanup. Because I wrote files each week there are some inefficiencies in the libraries. There are also things that are now fixed in Lean and mathlib (I used a version of mathlib frozen in early January so that Lean and mathlib could be installed in our computer labs and on student's computers).

#### Mario Carneiro (May 22 2020 at 19:53):

Patrick Massot said:

And I also wish people could stop teaching set theory bullshit to our students. I'm marking exams and I just saw. Let's fix $(f, g) \in \left(\mathbb R^{\mathbb R}\right)^2$ instead of $f, g : \mathbb R \to \mathbb R$...

Yes, the type theory minded students can write the much clearer "Let's fix $(f,g):(\mathbb{R}\to\mathbb{R})\times(\mathbb{R}\to\mathbb{R})$"...

#### Mario Carneiro (May 22 2020 at 19:54):

or $(f,g):2\to\mathbb{R}\to\mathbb{R}$ in some conventions

#### Patrick Massot (May 22 2020 at 20:01):

I think you first suggestion is much clearer than what I wrote. The second one however...

#### Sam Lichtenstein (May 22 2020 at 20:06):

I have a basic question about basic.lean in the CNG (sorry to coopt someone else's thread) -- when proving something is an instance, like in the example:

```
instance : comm_ring ℂ :=
begin
-- first the data
refine_struct {
zero := (0 : ℂ), add := (+), neg := has_neg.neg, one := 1, mul := (*),
..};
sorry,
```

I am curious how to get Lean to "autocomplete" the set of data that needs to be provided in `refine_struct { ... } `

. (By autocomplete, I don't mean that it will fill the data itself, just the list of fields that need to be defined, i.e. zero, add, neg, one, mul in this example.) I have a vague recollection reading somewhere on Zulip that there is some magic thing one can type that causes a little light bulb to show up. Is that the case, and what is the magic?

#### Alex J. Best (May 22 2020 at 20:08):

It's {! !}, which you can ask to fill in the skeleton for the structure under construction.

#### Sam Lichtenstein (May 22 2020 at 20:08):

ah great, I knew there was a ! involved, but didn't remember that you need two of them

thanks!

#### Alex J. Best (May 22 2020 at 20:08):

I'm not sure it works in tactic mode though.

So you'd need to do `instance : comm_ring ℂ :={! !}`

to generate the structure first, then move into refine_struct if you prefer.

#### Sam Lichtenstein (May 22 2020 at 20:10):

are there keybindings, or does one need to use the mouse to hover over the bulb and select from the dropdown? (I am using VSCode not emacs)

#### Gabriel Ebner (May 22 2020 at 20:11):

`ctrl+.`

#### Sam Lichtenstein (May 22 2020 at 20:12):

Gabriel, if I am between the {! and the !} and I type CTRL + "." (which I think is what you meant?), nothing seems to happen

#### Sam Lichtenstein (May 22 2020 at 20:13):

is it supposed to?

#### Patrick Massot (May 22 2020 at 20:14):

Yes

#### Patrick Massot (May 22 2020 at 20:15):

And I think it should work wherever Lean wants a term, so inside refine_struct should be ok

#### Sam Lichtenstein (May 22 2020 at 20:17):

ah, duh it's CMD+. on a mac

#### Sam Lichtenstein (May 22 2020 at 20:18):

but does not work in refine_struct{}

#### Mario Carneiro (May 22 2020 at 20:21):

I think you have to write `refine_struct {! !}`

#### Alex J. Best (May 22 2020 at 20:25):

Didn't seem to work after refine struct for me

#### Sam Lichtenstein (May 22 2020 at 20:25):

"no code actions available"

#### Bryan Gin-ge Chen (May 22 2020 at 20:40):

Hah, this seems to work:

```
import data.complex.basic
instance a : comm_ring ℂ :=
begin
-- first the data
refine_struct by exact {! !};
sorry,
end
```

#### Jalex Stark (May 22 2020 at 21:04):

I didn't know about `{!!}`

until now. `suggest`

is pretty good at filling the same purpose (and if there are lemmas around letting you construct with fewer arguments, suggest can find some of those too)

#### Patrick Lutz (May 28 2020 at 21:15):

I noticed that in the official solutions to the complex number game (which @Kevin Buzzard said were basically taken directly from mathlib) sometimes simp is used on a nonterminal line of a proof. For instance:

```
@[simp] lemma conj_add (z w : ℂ) : conj (z + w) = conj z + conj w :=
by ext; -- check on real and imag parts
simp; -- question becomes to check that a+b=b+a for certain real numbers a and b
ring -- true because this is obvious in a ring
```

Is this considered bad style, or is there a reason it's okay to do here?

#### Mario Carneiro (May 28 2020 at 21:17):

`simp, ring`

is a whitelisted combination

#### Mario Carneiro (May 28 2020 at 21:17):

because it is mostly insensitive to additional simp rules

#### Patrick Lutz (May 28 2020 at 21:18):

wouldn't there still be a problem if simp became good enough to finish the proof on its own? You're not allowed to have additional lines after the goals have been accomplished right?

#### Mario Carneiro (May 28 2020 at 21:19):

Indeed, `simp; ring`

is better than `simp, ring`

for this reason

#### Patrick Lutz (May 28 2020 at 21:20):

what's the difference between `,`

and `;`

exactly?

#### Mario Carneiro (May 28 2020 at 21:22):

`tac1;tac2`

calls `tac1`

and then calls `tac2`

on all goals produced by `tac1`

#### Alex J. Best (May 28 2020 at 21:22):

`,`

will do one tactic after the other, `;`

will run the second tactic on all the goals produced by the first (so if there are none it gracefully does nothing)

#### Patrick Lutz (May 28 2020 at 21:23):

Okay, I think I had missed that aspect of it

#### Patrick Lutz (May 28 2020 at 21:23):

Thanks

#### Alex J. Best (May 28 2020 at 21:23):

If you have an iff statement you might use `split; intro`

for example.

#### Reid Barton (May 28 2020 at 21:30):

If a proof breaks because it tries to invoke `ring`

when there are no goals, it's usually pretty obvious how to fix it.

#### Kevin Buzzard (May 28 2020 at 22:36):

I used `simp; linarith`

today and felt like I could get away with it for the same sort of reason

#### Filippo A. E. Nuccio (May 30 2020 at 13:27):

Kevin Buzzard said:

Filippo A. E. Nuccio I just pushed solutions to

`field.lean`

in the complex number game repo

I have finished playing with everything you proposed before proving that $\mathbb{C}$ is a field, and I am now trying to attack this. I realise I am stuck with inv, already, because I can't tell Lean how to distinguish between 0 and non-zero complex numbers. I have tried to copy from the proof that $\mathbb{Q}$ is a field, unfortunately with no success. In the link I had, I cannot really see your solutions, have you uploaded them or are you still beneath your pile of copies to be marked?

#### Alex J. Best (May 30 2020 at 13:32):

They are at https://github.com/ImperialCollegeLondon/complex-number-game/tree/master/kb_solutions

#### Filippo A. E. Nuccio (May 30 2020 at 13:33):

Ahah! Thanks, I had the wrong adress.

#### Kevin Buzzard (May 30 2020 at 13:41):

Sorry, my solutions are currently in flux because last Thursday I embarked upon a major refactor. What is going on here is that in src there are incomplete solutions to the current (re-ordered) state of the game, and Alex' link is to far more complete solutions to the older version of the game, which is basically exactly the same theorems but in a different order. Hope you can untangle things from these hints! To give an example of the difference: I moved the "coercion from R to C" level from level 4 to level 1, because it was quite boring and the sooner you do it the less you have to do; as a result any theorems about e.g. coercions and conjugation used to be in the coersions level and are now in the conjugation level (you need to have both the coercion and conjugation to formalise the statement, and because the order of the levels swapped, the level which the lemma appears in changes).

#### Kevin Buzzard (May 30 2020 at 13:41):

@Filippo A. E. Nuccio

#### Filippo A. E. Nuccio (May 30 2020 at 13:45):

Yes, thanks, I realised this. But it is OK, I could make my way through the solutions. I am now trying to digest your def's of inv and on how to prove that $\mathbb{C}$ is a field.

#### Kevin Buzzard (May 30 2020 at 14:46):

So what is going on here is that if z isn't 0 then my definition is mathematically correct, and if z=0 then the inverse is 0 because I am dividing by 0 and x/0=0. The key thing which is not obvious is that in Lean the axioms for a field contain this "inverse" map which is a map from K to K, defined by inv(0)=0 and then for non-zero z there's an axiom z*inv(z)=1. So it's just the same as a usual field but they totalised the inverse function, because total functions are easier to work with.

#### Jalex Stark (May 31 2020 at 01:07):

Filippo, do you know about tactic#by_cases? Maybe `by_cases z = 0`

is useful for the things you're working on

#### Filippo A. E. Nuccio (May 31 2020 at 09:57):

Well, but in the definition

```
noncomputable def inv (z : ℂ) : ℂ :=
⟨re(z)/norm_sq(z), -im(z)/norm_sq(z)⟩
```

where is it hidden that $z \ne 0$? Because although I can understand that you can insist $\mathrm{inv}(0)=0$ and set $z^{-1}=\mathrm{inv}(z)$, so that $0^{-1}=0$, the above definition involves dividing $0=\mathrm{re}(0)$ by $\mathrm{norm}\_\mathrm{sq}(0)$ as real numbers, no?

#### Kenny Lau (May 31 2020 at 09:58):

it isn't?

#### Filippo A. E. Nuccio (May 31 2020 at 09:58):

?

#### Kenny Lau (May 31 2020 at 09:59):

if `z=0`

then `inv 0 = \< re 0 / norm_sq 0, -im 0 / norm_sq 0 \> = \< 0 / 0, 0 / 0 \> = \< 0, 0 \> = 0`

#### Kenny Lau (May 31 2020 at 09:59):

where `0 / 0 = 0 * 0\-1 = 0 * 0 = 0`

#### Filippo A. E. Nuccio (May 31 2020 at 10:00):

Ah, so you are saying that it has already been declared that also in $\mathbb{R}$ we have $a/0=0$ for all $a\in\mathbb{R}$ and therefore the definition makes sense for all $z\in\mathbb{C}$?

#### Kenny Lau (May 31 2020 at 10:00):

yep

#### Filippo A. E. Nuccio (May 31 2020 at 10:00):

Great! Thanks.

#### Johan Commelin (May 31 2020 at 10:00):

It's a field "axiom"

#### Filippo A. E. Nuccio (May 31 2020 at 10:00):

Ah, perfect. And we're applying it to the reals to deduce it for the complexes

#### Kevin Buzzard (May 31 2020 at 10:08):

Filippo A. E. Nuccio said:

Ah, so you are saying that it has already been declared that also in $\mathbb{R}$ we have $a/0=0$ for all $a\in\mathbb{R}$ and therefore the definition makes sense for all $z\in\mathbb{C}$?

"In Lean the axioms for a field contain this "inverse" map which is a map from K to K, defined by inv(0)=0 and then ...", and the reals are already a field because I imported `data.real.basic`

which shows this.

#### Filippo A. E. Nuccio (May 31 2020 at 10:12):

Great, I was stupidly thinking that the "field" in the sentence was $\mathbb{C}$, whereas it was both $\mathbb{R}$ and $\mathbb{C}$...

#### Jalex Stark (Jun 01 2020 at 01:56):

`0\inv = 0`

is true not just in R or C, it's true in any field, where a field is the sort of thing talked about on this page: https://en.wikipedia.org/wiki/Field_(mathematics)

#### Yury G. Kudryashov (Jun 01 2020 at 02:09):

More precisely: `mathlib`

formalizes fields and division rings so that `0⁻¹=0`

. In math it is usually undefined.

#### ROCKY KAMEN-RUBIO (Jun 02 2020 at 19:17):

From the most recent version, it looks like `local attribute [simp] ext_iff `

is on line 58 of Kevin's solution to level 01, but not in either of the user solution files. It's not obvious to me that I would need to add this, and makes some of his solutions break if you keep the given files structure. Was there thing I missed that mentioned having to add this yourself?

#### Kevin Buzzard (Jun 02 2020 at 19:23):

I am in two minds about whether this is a good idea

#### Kevin Buzzard (Jun 02 2020 at 19:23):

If you make it a simp lemma then some low level proofs are easier but people seemed to think that it was not a good global simp lemma

#### Kevin Buzzard (Jun 02 2020 at 19:24):

Someone suggested that it was obfuscating the proofs

#### Kevin Buzzard (Jun 02 2020 at 19:24):

It was also making trivial proofs shorter

#### Kevin Buzzard (Jun 02 2020 at 19:25):

So either add it, or do ext; simp instead of simp

#### ROCKY KAMEN-RUBIO (Jun 02 2020 at 20:30):

oh ok, the earlier comments about this make more sense now.

#### Kevin Buzzard (Jun 03 2020 at 07:28):

Extensionality is the principle that two things are equal if they're made from the same parts. The extensionality tactic can be used to replace a goal that two things are equal by goals saying the parts are equal. `complex.ext`

is tagged with `@[ext]`

to make the extensionality tactic use this lemma. But it only goes one way. If you have a hypothesis that two complex numbers are equal and you want to deduce that their real and imaginary parts are equal I don't think you can use the `ext`

tactic, so that's why `ext_iff`

is useful. I realised I was using it a lot though so I wanted to teach it to `simp`

.

#### Mario Carneiro (Jun 03 2020 at 07:34):

If you have that two complex numbers are equal and want to know their real parts are equal, use `congr`

Last updated: May 12 2021 at 04:19 UTC