nnrat

Stream: condensed mathematics

[Yaël Dillies]

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]

I think so, yes.

[Bhavik Mehta]

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

[Yaël Dillies]

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

[Julian Külshammer]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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]

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