Zulip Chat Archive

Stream: condensed mathematics

Topic: nnrat


Yaël Dillies (Feb 17 2022 at 10:33):

I'm going to refactor nnrat to use nonneg in the next few days and PR it. Who should I credit? Mostly @Bhavik Mehta I presume?

Johan Commelin (Feb 17 2022 at 10:39):

I think so, yes.

Bhavik Mehta (Feb 17 2022 at 13:43):

It might also be worth crediting the authors of the nnreal stuff originally, since what I did was adapted from that

Yaël Dillies (Feb 17 2022 at 13:50):

Is there precedent for creditin through adaptation? Likely most boilerplate in mathlib is adapted from somewhere else.

Julian Külshammer (Feb 17 2022 at 13:54):

In other cases I mention such adaptation credit in implementation details, don't know whether this is standard in mathlib.

Bhavik Mehta (Feb 17 2022 at 17:18):

Perhaps not, but I would much rather err on the side of over-crediting than under-crediting

Kevin Buzzard (Feb 17 2022 at 21:00):

Patrick and I wrote quotient groups by copying what Johannes Hoelzl had done for quotient modules, and we mentioned this in the module docstring IIRC

Yaël Dillies (Feb 17 2022 at 21:02):

That makes more sense than marking as authors people who never touched the code.


Last updated: Dec 20 2023 at 11:08 UTC