Commit 2025-01-20 16:38 0fecf8fc

View on Github →

chore(100,1000.yaml): name the authors field 'authors' (#20875) Currently, there is some annoying inconsistency

  • the 1000 theorems project calls the field 'authors'
  • the 1000.yaml file calls it 'author', deviating from this
  • the 100.yaml file calls it 'author'. Change them all to 'authors' for consistency. Since formalisations are usually work of multiple people, this seems more appropriate, and matches the 1000+ theorem.

Estimated changes