mathlib3
7948b5a2 - chore(*): fix authorship for split files (#4480)

Commit
5 years ago
chore(*): fix authorship for split files (#4480) A few files with missing copyright headers in #4477 came from splitting up older files, so the attribution was incorrect: - `data/setoid/partition.lean` was split from `data/setoid.lean` in #2853. - `data/finset/order.lean` was split from `algebra/big_operators.lean` in #3495. - `group_theory/submonoid/operations.lean` was split from `group_theory/submonoid.lean` in #3058.
Parents
Loading