Zulip Chat Archive

Stream: PR reviews

Topic: determinants


view this post on Zulip Chris Hughes (Oct 07 2018 at 16:16):

I did some tidying on the determinants PR. I got rid of all the relics of Sym that weren't actually used for determinants - It's now only a 130 line Pr, versus 481. I also made the proofs hopefully more readable, if longer. Result is here https://github.com/leanprover/mathlib/compare/master...dorhinj:determinants2?expand=1

view this post on Zulip Chris Hughes (Oct 07 2018 at 16:17):

Old version https://github.com/leanprover/mathlib/pull/378/files

view this post on Zulip Mario Carneiro (Oct 08 2018 at 00:03):

is it PR'd? I want

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:25):

So now we have determinants, but we don't know that it is a monoid hom. For this we need https://github.com/leanprover/mathlib/pull/375

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:29):

I don't understand why that thing is called the free_module

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:29):

Should I just remove that code for now?

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:29):

The bit on scalar matrices is more important to me

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:30):

Why do we need it? Like I said diagonal subsumes it

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:30):

I think it is nice to have

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:31):

We also have a * I

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:31):

which is the way the rest of the world notates this

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:31):

Hmm... ok

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:31):

I don't really care

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:31):

I'm trying to understand what is needed

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:32):

What is needed is that det is a monoid hom

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:32):

That PR doesn't say anything about monoid homs

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:32):

No, but det_one uses det_scalar

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:32):

That stuff was commented out in my det PR

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:32):

I don't know if Chris preserved those comments. Let me check

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:33):

No, those are gone

view this post on Zulip Chris Hughes (Oct 08 2018 at 07:58):

We have det_one so it is proven to be a monoid hom. Are monoid Homs defined yet?

view this post on Zulip Johan Commelin (Oct 08 2018 at 08:00):

Yes they are

view this post on Zulip Johan Commelin (Oct 08 2018 at 08:00):

So my new PR is a 4-liner.


Last updated: May 06 2021 at 12:15 UTC