mathlib

5c0000c0 - chore(*): remove extra author info (#3051)

chore(*): remove extra author info (#3051) Removing changes to author headers in files with recent changes. Authorship should be cited in the headers only for significant contributions.