Skip to content

Commit

Permalink
doc(NumberTheory/Padics/MahlerBasis): add credit line (#19845)
Browse files Browse the repository at this point in the history
The file `NumberTheory/Padics/MahlerBasis.lean` is largely based on the ETH Zürich bachelor thesis of Giulio Caflisch. This PR gives Giulio due credit for this -- he is already included in the "Authors" line, but this does not appear in the online reference manual. I am following here the example of [JacobiSum/Basic](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/JacobiSum/Basic.html), which is likewise based on a bachelor thesis project.
  • Loading branch information
loefflerd committed Dec 10, 2024
1 parent 8544aa5 commit ebd71de
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions Mathlib/NumberTheory/Padics/MahlerBasis.lean
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,9 @@ converges (uniformly) to `f`, and this construction defines a Banach-space isomo
For this, we follow the argument of Bojanić [bojanic74].
The formalisation of Mahler's theorem presented here is based on code written by Giulio Caflisch
for his bachelor's thesis at ETH Zürich.
## References
* [R. Bojanić, *A simple proof of Mahler's theorem on approximation of continuous functions of a
Expand Down

0 comments on commit ebd71de

Please sign in to comment.