## Stream: kbb

### Topic: PRing

#### Johannes Hölzl (Sep 17 2018 at 09:41):

I'm a little bit lost:

• is @Kenny Lau 's Sym related to @Chris Hughes' group_theory.perm?
• do we need computable_matrix? there are a lot of definitions, do we need them now? I think we should think about this before we add them,
• determinants looks mostly good to me (modulo some naming, e.g. finset.prod_mul_right)
• holomorphic_function: I guess we can add complex_derivative and generalize it later?
• matrices is this Sean's version?
• monoid_stuff is good
• it would be good if all files get a header who was involved in them

#### Johan Commelin (Sep 17 2018 at 09:42):

matrices is indeed Sean's version.

#### Johan Commelin (Sep 17 2018 at 09:42):

I'm not sure if we need computable_matrix just now.

good

#### Johan Commelin (Sep 17 2018 at 09:46):

@Johannes Hölzl Thanks for this feedback.

#### Johan Commelin (Sep 17 2018 at 09:46):

What do you think of modular_group and SL2Z_generators? I guess those are "tricky" files...

#### Johannes Hölzl (Sep 17 2018 at 09:49):

modular_group look tidy to me. But I don't know a lot about the theory behind it

#### Johannes Hölzl (Sep 17 2018 at 09:49):

I don't know why some names end in an underscore like SL2Z_M_?

#### Johannes Hölzl (Sep 17 2018 at 09:57):

SL2Z_generators has some ugly proofs in it... I hope we can simplify them...

#### Johan Commelin (Sep 17 2018 at 11:46):

Hmm, the I am the one how wrote those underscore definitions. I cannot really give a precise reason for why I do it, but it is somehow intended to convey that the first argument is sort "fixed".

#### Johan Commelin (Sep 17 2018 at 11:46):

Like the $p$ in $\mathbb{Z}_p$

Last updated: May 18 2021 at 10:14 UTC