# Zulip Chat Archive

## Stream: maths

### Topic: with_bot

#### orlando (May 07 2020 at 18:33):

Hello,

I'm reading a little the theory of degree in `data.polynomial`

and there is a strange object : ` with_bot \N`

:sweat_smile:

Do you have an idea to deal with bot ? For example !

```
import order
open with_bot
example (a b : with_bot ℕ ) : a ≤ b → a+1 ≤ b+1 := begin
intros,
end
```

#### Mario Carneiro (May 07 2020 at 18:43):

what is `bot+1`

supposed to be in this statement?

#### Mario Carneiro (May 07 2020 at 18:43):

That's true as long as you are talking about nats, and nats embed in `with_bot nat`

#### orlando (May 07 2020 at 19:02):

Hello Mario,

For me `bot + 1 = bot `

so i each case it ok !

But i don't understand who to deal in lean ? Is there is a file where this arithmetic property are state ?

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

Just do cases on a and b?

#### orlando (May 07 2020 at 19:20):

Yep i can cases ... but but but :sweat_smile:

```
example (a b : with_bot ℕ ) : a ≤ b → a+1 ≤ b+1 := begin
rcases b, intros, rcases a, exact le_refl (none +1),
rw none_eq_bot at *, rw some_eq_coe at *,rw le_bot_iff at a_1,
rw a_1, refine le_refl _,
rcases a, rw none_eq_bot at *, rw some_eq_coe at *,
intros, exact bot_le, rcases a, intros,
rw some_eq_coe at *, erw zero_add,
not finish
```

#### Johan Commelin (May 07 2020 at 19:21):

@orlando Note that there is also `nat_degree`

.

#### Johan Commelin (May 07 2020 at 19:21):

They are the same, except for the zero polynomial

#### orlando (May 07 2020 at 19:24):

Yep Johan, but a try to use the theorem : in $$ \C $$ all polynomial of `0 < degree `

have roots ... and i have to deal i little with ` degree`

:confused:

#### orlando (May 07 2020 at 19:44):

I little better

```
example (a b : with_bot ℕ ) : a ≤ b → a+1 ≤ b+1 := begin
intros,
rcases b, intros, rcases a,
exact le_refl (none +1),
erw le_bot_iff at a_1, rw a_1,
refine le_refl _,
rcases a,
exact bot_le,
apply some_le_some.mpr, apply add_le_add,
apply some_le_some.mp a_1, exact le_refl 1,
end
```

#### Johan Commelin (May 07 2020 at 19:44):

@orlando There is a lemma `degree_eq_nat_degree`

, which is probably useful

#### Johan Commelin (May 07 2020 at 19:45):

Of course it comes with the assumption that the polynomial is not zero

#### orlando (May 07 2020 at 19:54):

perhaps it help me ! I'm trying to make caracteristic polynomial of a matrix. And i have to proof that the degree of the polynomial is equal to the dimension of the matrix.

#### Reid Barton (May 07 2020 at 20:05):

where is this `+`

even defined?

#### Kevin Buzzard (May 07 2020 at 20:06):

```
instance [add_semigroup α] : add_semigroup (with_bot α) := with_top.add_semigroup
```

#### Kevin Buzzard (May 07 2020 at 20:06):

```
instance [add_semigroup α] : add_semigroup (with_top α) :=
{ add := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b)),
..@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _ }
```

I blame Mario

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

I can't find `some x + some y = some (x+y)`

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

`norm_cast`

won't do it

#### Kevin Buzzard (May 07 2020 at 20:08):

```
import data.polynomial
open with_bot
#check with_bot.add_semigroup
example (a b : with_bot ℕ ) : a ≤ b → a+1 ≤ b+1 := begin
intro hab,
cases a with a; cases b with b,
{ refine le_refl _},
{ rw none_eq_bot,
rw bot_add,
refine bot_le},
{ exfalso,
rw none_eq_bot at hab,
rw le_bot_iff at hab,
cases hab},
{ rw some_le_some at hab,
show (a : with_bot ℕ) + (1 : ℕ) ≤ b + (1 : ℕ),
sorry
},
end
```

Everything else is easy

#### Reid Barton (May 07 2020 at 20:10):

Kevin Buzzard said:

`instance [add_semigroup α] : add_semigroup (with_bot α) := with_top.add_semigroup`

okay thanks, then the proof is `add_le_add_right'`

.

#### Kevin Buzzard (May 07 2020 at 20:10):

@orlando because you don't format your code properly it's difficult for other people to read. You should use `{}`

instead of having multiple goals open at once

#### Reid Barton (May 07 2020 at 20:10):

I don't know why `apply`

can't apply this or why `library_search`

can't find it though.

#### Kevin Buzzard (May 07 2020 at 20:13):

Orlando is doing induction on a but the issue isn't going to go away: the other goal is

```
b a : ℕ
⊢ some (nat.succ a) ≤ some b → some (nat.succ a) + 1 ≤ some b + 1
```

It all hinges on `some`

being a monoid hom.

#### Reid Barton (May 07 2020 at 20:13):

Reid Barton said:

I don't know why

`apply`

can't apply this

Aha, because `le`

is cleverly implemented as a forall/function.

#### Kevin Buzzard (May 07 2020 at 20:13):

aah, `coe_add`

isn't tagged with one of these `norm_cast`

tags.

#### Reid Barton (May 07 2020 at 20:14):

Why are you mucking around with casts and stuff?

#### Kevin Buzzard (May 07 2020 at 20:14):

because I couldn't find the algebraic class which with_bot nat was

#### Reid Barton (May 07 2020 at 20:15):

It's annoying how hard it is to find instances.

#### Kevin Buzzard (May 07 2020 at 20:15):

but you're right, it's an `ordered_add_comm_monoid`

.

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

```
import order
open with_bot
example (a b : with_bot ℕ) (H : a ≤ b) : a + 1 ≤ b +1 :=
begin
cases a with a,
{ exact bot_le },
{ rcases H a rfl with ⟨n, ⟨⟩, han⟩,
rintros m ⟨⟩,
exact ⟨n+1, rfl, nat.succ_le_succ han⟩ }
end
```

#### Reid Barton (May 07 2020 at 20:16):

my proof is shorter than kenny's :hole_in_one:

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

oh

#### Kevin Buzzard (May 07 2020 at 20:17):

```
with_bot.coe_le : ∀ {α : Type ?} [_inst_1 : partial_order α] {a b : α} {o : option α}, b ∈ o → (↑a ≤ o ↔ a ≤ b)
```

gaargh

#### Kevin Buzzard (May 07 2020 at 20:17):

that's not what `coe_le`

is supposed to say

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

proposition to make `\le`

inductive

#### Reid Barton (May 07 2020 at 20:19):

Hopefully it goes better than when I tried to do that to `continuous`

...

#### orlando (May 07 2020 at 20:22):

@Reid Barton ... ` add_le_add_right' `

:+1: :+1: :+1:

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

The trick is to realise that it's an `ordered_add_comm_monoid`

#### orlando (May 07 2020 at 20:23):

Yep Kevin ! That give property ! That good !

#### Kevin Buzzard (May 07 2020 at 20:33):

I see. So somehow the correct way to proceed would have been to say to Lean "hey Lean, give me the complete list of instances on `with_bot nat`

because I can't remember the axioms for half of them and so don't actually know if it's an ordered semigroup or even if Lean has ordered semigroups"

#### Reid Barton (May 07 2020 at 20:34):

Well, ideally `library_search`

would have simply worked but probably it ran into the apply bug

#### Reid Barton (May 07 2020 at 20:34):

But otherwise, yes that would be nice to have.

#### orlando (May 07 2020 at 20:37):

` libraty_search `

and `suggest `

are nice tactic !!!

#### Kevin Buzzard (May 07 2020 at 20:39):

"and then tell me all the lemmas which apply to that object". I see. That's what `library_search`

is supposed to do?

#### orlando (May 07 2020 at 20:42):

In 10 years lean will work on his own, we will just have to watch him prove theorems :grinning_face_with_smiling_eyes:

#### Mario Carneiro (May 07 2020 at 21:52):

Kevin Buzzard said:

I see. So somehow the correct way to proceed would have been to say to Lean "hey Lean, give me the complete list of instances on

`with_bot nat`

because I can't remember the axioms for half of them and so don't actually know if it's an ordered semigroup or even if Lean has ordered semigroups"

```
namespace tactic
meta def env_fold {α} (a : α) (f : declaration → α → tactic α) : tactic α :=
get_env >>= λ e s, e.fold ((return a : tactic _) s) $ λ d t,
interaction_monad.result.cases_on t (f d) result.exception
#print interaction_monad.monad
meta def get_all_classes : tactic (list name) :=
list.reverse <$> env_fold [] (λ d l,
mcond (is_class (expr.const d.to_name (level.param <$> d.univ_params)))
(return (d.to_name :: l)) (return l))
meta def list_instances (e : expr) : tactic (list expr) :=
get_all_classes >>= list.mfoldr (λ n l,
(do e' ← mk_app n [e],
mk_instance e' >> return (e' :: l)) <|>
return l) [] .
open interactive interactive.types
meta def interactive.list_instances (e : parse texpr) : tactic unit :=
to_expr e >>= list_instances >>= list.mmap' trace
run_cmd list_instances `(ℕ) >>= trace
example : true := by {list_instances ℕ, trivial}
end tactic
```

#### Mario Carneiro (May 07 2020 at 21:52):

```
add_semigroup ℕ
has_sub ℕ
inhabited ℕ
add_monoid ℕ
has_well_founded ℕ
semigroup ℕ
has_lt ℕ
has_to_tactic_format ℕ
decidable_linear_ordered_cancel_add_comm_monoid ℕ
has_to_format ℕ
has_one ℕ
monoid ℕ
preorder ℕ
add_comm_monoid ℕ
add_comm_semigroup ℕ
has_zero ℕ
has_mod ℕ
comm_semigroup ℕ
zero_ne_one_class ℕ
has_sizeof ℕ
reflected ℕ
has_le ℕ
has_repr ℕ
comm_monoid ℕ
nonempty ℕ
linear_order ℕ
distrib ℕ
has_to_string ℕ
add_right_cancel_semigroup ℕ
ordered_semiring ℕ
decidable_linear_order ℕ
has_add ℕ
mul_zero_class ℕ
has_dvd ℕ
semiring ℕ
has_mul ℕ
has_div ℕ
add_left_cancel_semigroup ℕ
decidable_linear_ordered_semiring ℕ
linear_ordered_semiring ℕ
ordered_cancel_add_comm_monoid ℕ
comm_semiring ℕ
partial_order ℕ
```

#### Mario Carneiro (May 07 2020 at 21:55):

```
example : true := by {list_instances (with_bot ℕ), trivial}
-- add_semigroup (with_bot ℕ)
-- inhabited (with_bot ℕ)
-- semilattice_sup_bot (with_bot ℕ)
-- add_monoid (with_bot ℕ)
-- has_well_founded (with_bot ℕ)
-- has_lt (with_bot ℕ)
-- has_to_tactic_format (with_bot ℕ)
-- lattice (with_bot ℕ)
-- has_sup (with_bot ℕ)
-- ordered_add_comm_monoid (with_bot ℕ)
-- has_to_format (with_bot ℕ)
-- has_one (with_bot ℕ)
-- distrib_lattice (with_bot ℕ)
-- preorder (with_bot ℕ)
-- add_comm_monoid (with_bot ℕ)
-- add_comm_semigroup (with_bot ℕ)
-- has_zero (with_bot ℕ)
-- has_bot (with_bot ℕ)
-- has_sizeof (with_bot ℕ)
-- semilattice_inf (with_bot ℕ)
-- reflected (with_bot ℕ)
-- has_le (with_bot ℕ)
-- nonempty (with_bot ℕ)
-- linear_order (with_bot ℕ)
-- decidable_linear_order (with_bot ℕ)
-- semilattice_inf_bot (with_bot ℕ)
-- has_add (with_bot ℕ)
-- semilattice_sup (with_bot ℕ)
-- has_inf (with_bot ℕ)
-- order_bot (with_bot ℕ)
-- partial_order (with_bot ℕ)
```

#### Kevin Buzzard (May 07 2020 at 22:54):

Oh this was the thing that was called ordered_comm_monoid which confused the perfectoid project? How come there's no ordered_monoid?

#### Johan Commelin (May 08 2020 at 03:48):

@Kevin Buzzard In mathlib/core what used to be called an `ordered_monoid`

is now called `ordered_add_monoid`

. Once `norm_num`

is out of core, we can refactor everything and also have (multiplicative) `ordered_monoid`

s.

Of course we could have them now, but not with all the nice `to_additive`

machinery. That's why the `norm_num`

PR is important.

#### Johan Commelin (May 08 2020 at 03:51):

Reid Barton said:

It's annoying how hard it is to find instances.

With the new widget stuff by @Edward Ayers this will hopefully be a lot easier soon. It's really ironic that the goal window has all this information (in principle), but is only showing us a really nice `pp`

version. And if you ask for the raw stuff, that's what you get. A brutal flood of :poop: (-;

Anyway, in the mean time: what about a command `#find_instance`

that just like `#simp`

uses variables that have been declared in the context, so that you can do things like

```
#find_instance : add_comm_monoid (with_bot nat)
variables (X Y : Type) [fintype X] [fintype Y]
#find_instance : fintype (X → Y)
```

etc...

#### orlando (May 08 2020 at 23:05):

Hello, just to understand the mecanism of coersion. Is there is a quick way to do that ?

```
lemma cast_bot' (a : ℕ ) : nat.cast (a) = ( a: with_bot ℕ ) := ???
```

#### Chris Hughes (May 08 2020 at 23:24):

If you had used the notation for `nat.cast`

I think `simp`

would solve it. Otherwise, I think it would have to be done by induction on `a`

if it isn't in the library.

#### Chris Hughes (May 08 2020 at 23:26):

There's two coercion from nat to `with_bot nat`

, and you should usually just use the higher priority `with_bot`

coercion. Most of the necessary lemmas are in the `with_bot`

namespace.

#### orlando (May 09 2020 at 00:04):

Ok for the two coersion, so the definition is ` with_bot`

not `nat.cast `

! Thx !

#### Kevin Buzzard (May 09 2020 at 07:16):

I think the trick is to find out which one is used in the library and then to always use that one, and to always use it in the exact syntactic form which is in the library, because if you don't then `simp`

will not work

#### orlando (May 09 2020 at 07:37):

@Kevin Buzzard : In theory, i understand ! But i practice i have some difficulty for example at the last proof i can't finish the proof without a conversion ` int.cast vs bot_cast `

.

The tactic state before ` cast_with_bot `

is

```
1 goal
R : Type u,
_inst_1 : nonzero_comm_ring R,
A : Type v,
_inst_2 : fintype A,
_inst_3 : decidable_eq A,
s : finset A,
φ : A → polynomial R,
hyp : ∀ (ℓ : A), degree (φ ℓ) = 1,
hyp_lc : ∀ (ℓ : A), monic (φ ℓ),
⊢ ↑(card s) = ↑(card s) ----- AHHAHAHAHAHAHAHAH :upside_down:
```

```
import data.polynomial
open finset polynomial with_bot
universes u v
variables
{R : Type u}[nonzero_comm_ring R]
{A : Type v} [fintype A][decidable_eq A]
lemma prod_monic (s : finset A)(φ : A → polynomial R) (hyp : ∀ a : A, monic (φ a)) :
monic (finset.prod s (λ x : A, φ x)) :=
begin
apply (finset.induction_on s), {
erw prod_empty at *,
exact leading_coeff_C _,
},
{
intros ℓ s hyp' hyp_rec,
rw finset.prod_insert (by assumption),
exact monic_mul (hyp ℓ) hyp_rec,
},
end
lemma degree_prod_monic (s : finset A)(φ : A → polynomial R)
(hyp_lc : ∀ ℓ : A, monic (φ ℓ )) :
degree (finset.prod s (λ x : A, φ x)) = finset.sum s ( λ x : A, degree (φ x)) :=
begin
apply (finset.induction_on s), {
rw prod_empty,
exact degree_C (one_ne_zero),
},
{
intros ℓ s hyp' hyp_rec,
rw finset.prod_insert (by assumption),
rw finset.sum_insert (by assumption),
rw ← hyp_rec,
apply degree_mul_eq',
conv_lhs {
rw monic.def.mp (hyp_lc ℓ), rw one_mul,
rw monic.def.mp (prod_monic s φ hyp_lc),
},
exact one_ne_zero,
},
end
theorem cast_with_bot (a : ℕ ) : nat.cast (a) = (a: with_bot ℕ ) := begin
apply (nat.rec_on a), {
exact rfl,
},
intros ℓ hyp_rec,
change _ = ↑ℓ + ↑1,
erw ← hyp_rec, exact rfl,
end
lemma coeff_prod_nat' (s : finset A)(φ : A → polynomial R)(hyp : ∀ ℓ : A, degree(φ ℓ ) = 1 )
(hyp_lc : ∀ ℓ : A, monic(φ ℓ) ) : -- monic !
degree (finset.prod s (λ x : A, φ x)) = card s :=
begin
rw degree_prod_monic s φ hyp_lc,
conv_lhs{
apply_congr, skip,
rw hyp x,
},
rw finset.sum_const, rw add_monoid.smul_one,
---- here i have to use nat.cast = with_bot coe HERE
refine cast_with_bot _ ,
end
```

#### Kevin Buzzard (May 09 2020 at 07:40):

Maybe sometimes it is unavoidable?

#### Kevin Buzzard (May 09 2020 at 07:41):

Maybe there is a missing `simp`

lemma though?

#### Kevin Buzzard (May 09 2020 at 07:42):

I am not an expert in `simp`

but maybe one should expect `norm_cast`

to solve this. Unfortunately I just regard `norm_cast`

as magic

#### orlando (May 09 2020 at 07:43):

i try all the ` simp hint library_search and suggest `

before understanding that the first coersion is `nat.cast`

and the second `bot_cast `

#### Kevin Buzzard (May 09 2020 at 07:43):

So I don't know whether `norm_cast`

should be taught to solve this or whether it is not its job

#### orlando (May 09 2020 at 07:43):

` hint `

give me a command`unfold_coes `

:grinning_face_with_smiling_eyes:

#### Mario Carneiro (May 09 2020 at 07:43):

there should be a theorem that says they are the same

#### Kevin Buzzard (May 09 2020 at 07:44):

But should the user be required to know its name?

#### Mario Carneiro (May 09 2020 at 07:44):

first the theorem, then the fancy

#### Kevin Buzzard (May 09 2020 at 07:44):

Because I am always confused about whether it's cast or coe, and which namespace it's in

#### Mario Carneiro (May 09 2020 at 07:44):

are we sure the theorem even exists?

#### Mario Carneiro (May 09 2020 at 07:45):

because if it doesn't I won't expect the tactics to find the proof

#### Kevin Buzzard (May 09 2020 at 07:45):

I don't know enough about `simp`

to know how to even state the lemma

#### Mario Carneiro (May 09 2020 at 07:46):

I don't know exactly what the lemma is here, something about with_bot?

#### orlando (May 09 2020 at 07:46):

i don't see ` nat.coe = bot_coe `

theorem in mathlib

#### Mario Carneiro (May 09 2020 at 07:47):

does that even typecheck?

#### Kevin Buzzard (May 09 2020 at 07:47):

This is all part of the CS machinery which I don't have much of an understanding of. I am not even 100% sure that `norm_cast`

should do it, but I guess that would be my instinct

#### Mario Carneiro (May 09 2020 at 07:47):

what are the types

#### Kevin Buzzard (May 09 2020 at 07:47):

And I wouldn't know how to make it do it if it didn't

#### Mario Carneiro (May 09 2020 at 07:47):

there is a mathematical part of this to be dealt with before the tactics can take over

#### orlando (May 09 2020 at 07:48):

This is ok

```
theorem cast_with_bot (a : ℕ ) : nat.cast (a) = (a: with_bot ℕ ) := begin
apply (nat.rec_on a), {
exact rfl,
},
intros ℓ hyp_rec,
change _ = ↑ℓ + ↑1,
erw ← hyp_rec, exact rfl,
end
```

#### Mario Carneiro (May 09 2020 at 07:48):

just over nat though?

#### Mario Carneiro (May 09 2020 at 08:17):

#### Mario Carneiro (May 09 2020 at 08:18):

It's apparently not eligible for any kind of `*_cast`

tactic, but it can be a simp lemma

#### orlando (May 09 2020 at 18:07):

Youppi : i finish the first part of caracteristic polynomial :grinning_face_with_smiling_eyes:

```
theorem (hyp : 0 < fintype.card A ): ∀ M : matrix A A ℂ , ∃ t : ℂ, det ( M + t •(1 : matrix A A ℂ )) = 0
```

#### Johan Commelin (May 09 2020 at 18:08):

Congratulations!

#### Johan Commelin (May 09 2020 at 18:08):

So now we know that eigenvalues exist (-;

#### Johan Commelin (May 09 2020 at 18:09):

What is the determinant of a 0x0 matrix?

#### Johan Commelin (May 09 2020 at 18:09):

I guess it's 1

#### Kenny Lau (May 09 2020 at 18:10):

Johan Commelin said:

So now we know that eigenvalues exist (-;

we don't know that C is alg. closed

#### Johan Commelin (May 09 2020 at 18:10):

We do

#### Johan Commelin (May 09 2020 at 18:10):

Chris did that ages ago

#### Kenny Lau (May 09 2020 at 18:10):

Johan Commelin said:

I guess it's 1

yes

#### Kenny Lau (May 09 2020 at 18:11):

Johan Commelin said:

Chris did that ages ago

wait what

#### Johan Commelin (May 09 2020 at 18:11):

We don't have algebraic closures, but we do know what an algebraically closed field is

#### orlando (May 09 2020 at 18:11):

@Johan Commelin hum : it's a sum over the permutation of empty set ... so a sum with one term ! so it's one i think !

#### Johan Commelin (May 09 2020 at 18:11):

Maybe we don't have a type class `[algebraically_closed K]`

, but we have FTA

#### Johan Commelin (May 09 2020 at 18:12):

@orlando Does your proof work for arbitrary alg closed fields?

#### Johan Commelin (May 09 2020 at 18:12):

If so, we quickly need to add that typeclass

#### orlando (May 09 2020 at 18:13):

The theorem FTA i s in the file : The theorem is in the file ` analysis.complex.polynomial `

#### orlando (May 09 2020 at 18:14):

Yes a think it's ok for all algebraicly closed field

#### Kenny Lau (May 09 2020 at 18:14):

what was the proof?

#### Johan Commelin (May 09 2020 at 18:14):

Of what?

#### Johan Commelin (May 09 2020 at 18:14):

@orlando Are you planning to PR this?

#### Kenny Lau (May 09 2020 at 18:15):

of FTA

#### Johan Commelin (May 09 2020 at 18:15):

@Chris Hughes :up:

#### Bhavik Mehta (May 09 2020 at 18:16):

Congratulations!!

#### orlando (May 09 2020 at 18:17):

@Johan Commelin : i have to simplify ! It's very complicated with the sum and the product of the determinant.

Thx @Bhavik Mehta :grinning:

#### Chris Hughes (May 09 2020 at 18:17):

I think there's even a link to the proof I used in the file. I did it well over a year ago.

#### Kenny Lau (May 09 2020 at 18:17):

yeah you linked to https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#classical_fta_via_advanced_calculus

#### Kenny Lau (May 09 2020 at 18:17):

aha, you proof the open mapping theorem specifically for polynomials

#### Kenny Lau (May 09 2020 at 18:18):

which does not require complex analysis

#### Kenny Lau (May 09 2020 at 18:18):

therefore the minimum (which exists by O analysis) must be 0

#### Johan Commelin (May 09 2020 at 18:22):

@orlando I strongly encourage you to PR this

#### Johan Commelin (May 09 2020 at 18:25):

`theorem jenesaispas`

, nice (-;

It will need some cleaning up and unfrenchyfying :rofl:

#### Mario Carneiro (May 09 2020 at 18:34):

Shouldn't that be `theorem je_ne_sais_pas`

?

#### Johan Commelin (May 09 2020 at 18:35):

Je ne sais pas...

#### orlando (May 09 2020 at 18:39):

I have no idea of name at the end :joy:

#### Patrick Massot (May 09 2020 at 20:28):

Johan Commelin said:

So now we know that eigenvalues exist (-;

Isn't it sad to use determinants for that?

#### Patrick Massot (May 09 2020 at 20:29):

Congratulations to Orlando anway!

#### Patrick Massot (May 09 2020 at 20:30):

Now you can start a very important part of your initiation to Lean. Turning this mess into a merged mathlib PR will teach you at least as much Lean as what you learned up to now.

#### Bhavik Mehta (May 09 2020 at 20:45):

Patrick Massot said:

Now you can start a very important part of your initiation to Lean. Turning this mess into a merged mathlib PR will teach you at least as much Lean as what you learned up to now.

I couldn't agree with this more!

#### orlando (May 09 2020 at 21:13):

@Patrick Massot : There is a long way to go to understand lean and mathlib. I have been using lean for two months and even if I have made progress, I am not really comfortable with it! Always a feeling of not understanding how it works. But that fun and i have time :grinning_face_with_smiling_eyes:

#### Kevin Buzzard (May 09 2020 at 22:06):

My first PR was the complex numbers and it got changed a huge amount before it was accepted. It's a very interesting experience!

Last updated: May 06 2021 at 17:38 UTC