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>
leanprover-community · Sep 23, 2021 · d238087 · d238087
1 parent a15ae9c
commit d238087
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/data/real/pi/bounds.lean b/src/data/real/pi/bounds.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Benjamin Davidson
+Authors: Floris van Doorn, Mario Carneiro
 -/
 import analysis.special_functions.trigonometric
 

diff --git a/src/data/real/pi/leibniz.lean b/src/data/real/pi/leibniz.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2019 Floris van Doorn. All rights reserved.
+Copyright (c) 2020 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Benjamin Davidson
+Authors: Benjamin Davidson
 -/
 import analysis.special_functions.pow
 

diff --git a/src/data/real/pi/wallis.lean b/src/data/real/pi/wallis.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2019 Floris van Doorn. All rights reserved.
+Copyright (c) 2021 Hanting Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Benjamin Davidson
+Authors: Hanting Zhang
 -/
 import analysis.special_functions.integrals