Zulip Chat Archive

Stream: kbb

Topic: merging into mathlib


view this post on Zulip Johan Commelin (Sep 24 2018 at 16:02):

Clearly some parts of kbb are not mathlib-ready, but other parts are.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:02):

I think we should try to get those merged into mathlib.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:03):

For example, the remainder of the file on matrices. The monoid stuff, and determinants should also be merge-ready, I think.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:04):

I'll try to work on this when I'm back home. This is a mental note for me, and a hint for others to possible help with this (-;

view this post on Zulip Johannes Hölzl (Sep 24 2018 at 17:09):

I will merge the PID -> UFD part

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:20):

Just to note here that Chris defined log as the unique inverse of exp yesterday, and proved exp log = id, log exp = id on the appropriate domains. @Chris Hughes Is this file publically accessible?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:22):

Nice! Is this the real version or the complex version?

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:23):

real single-valued log from positive reals to reals

view this post on Zulip Chris Hughes (Sep 25 2018 at 19:20):

@Kevin Buzzard Yes it is, on the exp branch of community mathlib.

view this post on Zulip Johan Commelin (Sep 27 2018 at 07:17):

@Scott Morrison Do you want to PR the category of matrices? Or would you like me to do it (from community mathlib)?

view this post on Zulip Johan Commelin (Sep 27 2018 at 07:17):

@Kenny Lau Do you want to PR determinants? Or would you like me to do it (from community mathlib)?

view this post on Zulip Scott Morrison (Sep 27 2018 at 07:18):

I'm certainly happy if you want to do it. :-) I have a lot of open PRs at the moment...

view this post on Zulip Scott Morrison (Sep 27 2018 at 07:31):

I do kind of like the

def free_module (α : Type v) [semiring α] : Type := ℕ
instance : category (free_module α) :=
{ hom  := λ m n, matrix (fin m) (fin n) α, ... }

It's somehow alien and familiar at the same time.

view this post on Zulip Mario Carneiro (Sep 27 2018 at 07:34):

I changed it to a large category over fintypes, what do you think?

view this post on Zulip Johan Commelin (Sep 27 2018 at 08:12):

@Mario Carneiro You also deleted a bunch of stuff on diagonal matrices, I think. Was that intentional?

view this post on Zulip Mario Carneiro (Sep 27 2018 at 08:12):

it all moved to mathlib

view this post on Zulip Johan Commelin (Sep 27 2018 at 08:19):

Hmmm, but not community mathlib...

view this post on Zulip Mario Carneiro (Sep 27 2018 at 08:21):

huh? just update master in that case

view this post on Zulip Chris Hughes (Sep 27 2018 at 08:23):

Or update the matrix branch

view this post on Zulip Johan Commelin (Sep 27 2018 at 09:10):

Aaah, I see what went wrong (and I was afk for 30 minutes)

view this post on Zulip Johan Commelin (Sep 27 2018 at 09:10):

@Mario Carneiro Is there a reason why you didn't merge scalar matrices?

view this post on Zulip Johan Commelin (Sep 27 2018 at 09:10):

Do you think they are not useful enough, because diagonal easily covers those cases?

view this post on Zulip Kenny Lau (Sep 27 2018 at 18:17):

@Kenny Lau Do you want to PR determinants? Or would you like me to do it (from community mathlib)?

please do it

view this post on Zulip Johan Commelin (Sep 27 2018 at 18:18):

I'll do it tomorrow

view this post on Zulip Mario Carneiro (Sep 27 2018 at 21:47):

Aren't there two different definitions of permutation sign (one over fin n, one over a fintype) right now? I think one was developed in kbb by Kenny and the other was in a mathlib PR by Chris

view this post on Zulip Kenny Lau (Sep 28 2018 at 04:47):

I'll do it tomorrow

the same time as when everyone does everything :p

view this post on Zulip Johan Commelin (Sep 28 2018 at 05:10):

I promise!

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:20):

@Kenny Lau Done.

view this post on Zulip Chris Hughes (Sep 28 2018 at 09:02):

@Johan Commelin @Kenny Lau fintype perm is in mathlib now by the way, I imagine you need that.

view this post on Zulip Johan Commelin (Sep 28 2018 at 09:06):

Aah, I just dumped Kenny's sym into the PR. Does this mean that stuff is duplicated?

view this post on Zulip Chris Hughes (Sep 28 2018 at 09:07):

Probably

view this post on Zulip Chris Hughes (Sep 28 2018 at 09:08):

Kenny did sign and stuff, which is also in mathlib.


Last updated: May 18 2021 at 11:11 UTC