Author on normal.lean?

Stream: general

[Thomas Browning]

The recent discussions on authors got me thinking. The last 75% of normal.lean was originally contributed by Patrick Lutz and I as part of the abel-ruffini project. Should I add our names to the authors list so that it's clear who to contact about that stuff?

[Johan Commelin]

I certainly think that the two of you deserve to be on that list (-;

[Scott Morrison]

Maybe we should be thinking of the Authors: list more as "these are the people on the hook when problems come up". So "deserve" is a loaded term. :-)

[Mario Carneiro]

I think the people on the hook when problems come up are the maintainers. Stuff that will cause problems for the maintainers are supposed to be caught during review