Zulip Chat Archive

Stream: PR reviews

Topic: determinants

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

Chris Hughes (Oct 07 2018 at 16:17):

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

Mario Carneiro (Oct 08 2018 at 00:03):

is it PR'd? I want

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

Mario Carneiro (Oct 08 2018 at 07:29):

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

Johan Commelin (Oct 08 2018 at 07:29):

Should I just remove that code for now?

Johan Commelin (Oct 08 2018 at 07:29):

The bit on scalar matrices is more important to me

Mario Carneiro (Oct 08 2018 at 07:30):

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

Johan Commelin (Oct 08 2018 at 07:30):

I think it is nice to have

Mario Carneiro (Oct 08 2018 at 07:31):

We also have a * I

Mario Carneiro (Oct 08 2018 at 07:31):

which is the way the rest of the world notates this

Johan Commelin (Oct 08 2018 at 07:31):

Hmm... ok

Johan Commelin (Oct 08 2018 at 07:31):

I don't really care

Mario Carneiro (Oct 08 2018 at 07:31):

I'm trying to understand what is needed

Johan Commelin (Oct 08 2018 at 07:32):

What is needed is that det is a monoid hom

Mario Carneiro (Oct 08 2018 at 07:32):

That PR doesn't say anything about monoid homs

Johan Commelin (Oct 08 2018 at 07:32):

No, but det_one uses det_scalar

Johan Commelin (Oct 08 2018 at 07:32):

That stuff was commented out in my det PR

Johan Commelin (Oct 08 2018 at 07:32):

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

Johan Commelin (Oct 08 2018 at 07:33):

No, those are gone

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?

Johan Commelin (Oct 08 2018 at 08:00):

Yes they are

Johan Commelin (Oct 08 2018 at 08:00):

So my new PR is a 4-liner.

Last updated: Dec 20 2023 at 11:08 UTC