## 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

#### 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

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?

Yes they are

#### 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