Zulip Chat Archive

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.

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

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 pp in Zp\mathbb{Z}_p

Last updated: Dec 20 2023 at 11:08 UTC