mathlib3
d238087f - chore(data/real/pi/*): correct authorship data (#9314)

Commit
4 years ago
chore(data/real/pi/*): correct authorship data (#9314) #9295 split `data.real.pi` into three files with the naive transferral of authorship and copyright data, this updates it to the actual authorship. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading