Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
doc(number_theory/padics/*): typo in references (#12229)
Browse files Browse the repository at this point in the history
Fix typos in a reference.
  • Loading branch information
kbuzzard committed Feb 23, 2022
1 parent 4238868 commit 7cc4eb9
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion src/number_theory/padics/padic_integers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ Coercions into `ℤ_p` are set up to work with the `norm_cast` tactic.
## References
* [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997]
* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
* <https://en.wikipedia.org/wiki/P-adic_number>
Expand Down
2 changes: 1 addition & 1 deletion src/number_theory/padics/padic_norm.lean
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ by taking `[fact (prime p)]` as a type class argument.
## References
* [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997]
* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
* <https://en.wikipedia.org/wiki/P-adic_number>
Expand Down
2 changes: 1 addition & 1 deletion src/number_theory/padics/padic_numbers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ Coercions from `ℚ` to `ℚ_p` are set up to work with the `norm_cast` tactic.
## References
* [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997]
* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
* <https://en.wikipedia.org/wiki/P-adic_number>
Expand Down

0 comments on commit 7cc4eb9

Please sign in to comment.