Zulip Chat Archive

Stream: maths

Topic: with_bot


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

view this post on Zulip Mario Carneiro (May 07 2020 at 18:43):

what is bot+1 supposed to be in this statement?

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

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 19:06):

Just do cases on a and b?

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

view this post on Zulip Johan Commelin (May 07 2020 at 19:21):

@orlando Note that there is also nat_degree.

view this post on Zulip Johan Commelin (May 07 2020 at 19:21):

They are the same, except for the zero polynomial

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

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

view this post on Zulip Johan Commelin (May 07 2020 at 19:44):

@orlando There is a lemma degree_eq_nat_degree, which is probably useful

view this post on Zulip Johan Commelin (May 07 2020 at 19:45):

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

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

view this post on Zulip Reid Barton (May 07 2020 at 20:05):

where is this + even defined?

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:06):

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

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:07):

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:07):

norm_cast won't do it

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:13):

aah, coe_add isn't tagged with one of these norm_cast tags.

view this post on Zulip Reid Barton (May 07 2020 at 20:14):

Why are you mucking around with casts and stuff?

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:14):

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

view this post on Zulip Reid Barton (May 07 2020 at 20:15):

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:15):

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

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

view this post on Zulip Reid Barton (May 07 2020 at 20:16):

my proof is shorter than kenny's :hole_in_one:

view this post on Zulip Kenny Lau (May 07 2020 at 20:16):

oh

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:17):

that's not what coe_le is supposed to say

view this post on Zulip Kenny Lau (May 07 2020 at 20:18):

proposition to make \le inductive

view this post on Zulip Reid Barton (May 07 2020 at 20:19):

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

view this post on Zulip orlando (May 07 2020 at 20:22):

@Reid Barton ... add_le_add_right' :+1: :+1: :+1:

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:22):

The trick is to realise that it's an ordered_add_comm_monoid

view this post on Zulip orlando (May 07 2020 at 20:23):

Yep Kevin ! That give property ! That good !

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

view this post on Zulip Reid Barton (May 07 2020 at 20:34):

Well, ideally library_search would have simply worked but probably it ran into the apply bug

view this post on Zulip Reid Barton (May 07 2020 at 20:34):

But otherwise, yes that would be nice to have.

view this post on Zulip orlando (May 07 2020 at 20:37):

libraty_search and suggest are nice tactic !!!

view this post on Zulip 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_searchis supposed to do?

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

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

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

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

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

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

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

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

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

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

view this post on Zulip orlando (May 09 2020 at 00:04):

Ok for the two coersion, so the definition is with_bot not nat.cast ! Thx !

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

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:40):

Maybe sometimes it is unavoidable?

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:41):

Maybe there is a missing simp lemma though?

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

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

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

view this post on Zulip orlando (May 09 2020 at 07:43):

hint give me a commandunfold_coes :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (May 09 2020 at 07:43):

there should be a theorem that says they are the same

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:44):

But should the user be required to know its name?

view this post on Zulip Mario Carneiro (May 09 2020 at 07:44):

first the theorem, then the fancy

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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:44):

are we sure the theorem even exists?

view this post on Zulip Mario Carneiro (May 09 2020 at 07:45):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:45):

I don't know enough about simp to know how to even state the lemma

view this post on Zulip Mario Carneiro (May 09 2020 at 07:46):

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

view this post on Zulip orlando (May 09 2020 at 07:46):

i don't see nat.coe = bot_coe theorem in mathlib

view this post on Zulip Mario Carneiro (May 09 2020 at 07:47):

does that even typecheck?

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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:47):

what are the types

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:47):

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

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

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

view this post on Zulip Mario Carneiro (May 09 2020 at 07:48):

just over nat though?

view this post on Zulip Mario Carneiro (May 09 2020 at 08:17):

#2636

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

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

view this post on Zulip Johan Commelin (May 09 2020 at 18:08):

Congratulations!

view this post on Zulip Johan Commelin (May 09 2020 at 18:08):

So now we know that eigenvalues exist (-;

view this post on Zulip Johan Commelin (May 09 2020 at 18:09):

What is the determinant of a 0x0 matrix?

view this post on Zulip Johan Commelin (May 09 2020 at 18:09):

I guess it's 1

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

view this post on Zulip Johan Commelin (May 09 2020 at 18:10):

We do

view this post on Zulip Johan Commelin (May 09 2020 at 18:10):

Chris did that ages ago

view this post on Zulip Kenny Lau (May 09 2020 at 18:10):

Johan Commelin said:

I guess it's 1

yes

view this post on Zulip Kenny Lau (May 09 2020 at 18:11):

Johan Commelin said:

Chris did that ages ago

wait what

view this post on Zulip Johan Commelin (May 09 2020 at 18:11):

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

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

view this post on Zulip Johan Commelin (May 09 2020 at 18:11):

Maybe we don't have a type class [algebraically_closed K], but we have FTA

view this post on Zulip Johan Commelin (May 09 2020 at 18:12):

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

view this post on Zulip Johan Commelin (May 09 2020 at 18:12):

If so, we quickly need to add that typeclass

view this post on Zulip orlando (May 09 2020 at 18:13):

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

view this post on Zulip orlando (May 09 2020 at 18:14):

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

view this post on Zulip Kenny Lau (May 09 2020 at 18:14):

what was the proof?

view this post on Zulip Johan Commelin (May 09 2020 at 18:14):

Of what?

view this post on Zulip Johan Commelin (May 09 2020 at 18:14):

@orlando Are you planning to PR this?

view this post on Zulip Kenny Lau (May 09 2020 at 18:15):

of FTA

view this post on Zulip Johan Commelin (May 09 2020 at 18:15):

@Chris Hughes :up:

view this post on Zulip Bhavik Mehta (May 09 2020 at 18:16):

Congratulations!!

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

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

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

view this post on Zulip Kenny Lau (May 09 2020 at 18:17):

aha, you proof the open mapping theorem specifically for polynomials

view this post on Zulip Kenny Lau (May 09 2020 at 18:18):

which does not require complex analysis

view this post on Zulip Kenny Lau (May 09 2020 at 18:18):

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

view this post on Zulip Johan Commelin (May 09 2020 at 18:22):

@orlando I strongly encourage you to PR this

view this post on Zulip Johan Commelin (May 09 2020 at 18:25):

theorem jenesaispas, nice (-;
It will need some cleaning up and unfrenchyfying :rofl:

view this post on Zulip Mario Carneiro (May 09 2020 at 18:34):

Shouldn't that be theorem je_ne_sais_pas?

view this post on Zulip Johan Commelin (May 09 2020 at 18:35):

Je ne sais pas...

view this post on Zulip orlando (May 09 2020 at 18:39):

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

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

view this post on Zulip Patrick Massot (May 09 2020 at 20:29):

Congratulations to Orlando anway!

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

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

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

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