Skip to content

Commit 0f2ba92

Browse files
committed
doc: wrap URL in angle brackets (leanprover-community#32556)
Otherwise `doc-gen` splits some URLs inappropriately.
1 parent f66351d commit 0f2ba92

1 file changed

Lines changed: 5 additions & 5 deletions

File tree

Counterexamples/EulerSumOfPowers.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ lemma sumOfPowersConjecture_of_injective {R S : Type*} [Semiring R] [Semiring S]
8888
/--
8989
The first counterexample was found by Leon J. Lander and Thomas R. Parkin in 1966
9090
through a computer search, disproving the conjecture.
91-
https://www.ams.org/journals/bull/1966-72-06/S0002-9904-1966-11654-3/S0002-9904-1966-11654-3.pdf
91+
<https://www.ams.org/journals/bull/1966-72-06/S0002-9904-1966-11654-3/S0002-9904-1966-11654-3.pdf>
9292
This is also the smallest counterexample for `n = 5`.
9393
-/
9494
theorem sumOfPowersConjectureFor_five_false : ¬SumOfPowersConjectureFor 5 := by
@@ -101,11 +101,11 @@ theorem sumOfPowersConjectureFor_five_false : ¬SumOfPowersConjectureFor 5 := by
101101
/--
102102
The first counterexample for `n = 4` was found by Noam D. Elkies in October 1988:
103103
`a := [2_682_440, 15_365_639, 18_796_760]`, `b := 20_615_673`
104-
https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf
104+
<https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf>
105105
In this paper, Elkies constructs infinitely many solutions to `a^4 + b^4 + c^4 = d^4` for coprime
106106
`a, b, c, d`, which provide infinitely many coprime counterexamples for the case `n = 4`.
107107
Here we use the smallest counterexample for `n = 4`, which was found a month later by Roger E. Frye
108-
https://ieeexplore.ieee.org/document/74138
108+
<https://ieeexplore.ieee.org/document/74138>
109109
-/
110110
theorem sumOfPowersConjectureFor_four_false : ¬SumOfPowersConjectureFor 4 := by
111111
intro conj
@@ -136,8 +136,8 @@ theorem existsEqualSumsOfLikePowersFor_of_sumOfPowersConjectureWith (R : Type*)
136136
After the first counterexample was found, Leon J. Lander, Thomas R. Parkin, and John Selfridge
137137
made a similar conjecture that is not amenable to the counterexamples found so far.
138138
The status of this conjecture is unknown.
139-
https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture
140-
https://www.ams.org/journals/mcom/1967-21-099/S0025-5718-1967-0222008-0/S0025-5718-1967-0222008-0.pdf
139+
<https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture>
140+
<https://www.ams.org/journals/mcom/1967-21-099/S0025-5718-1967-0222008-0/S0025-5718-1967-0222008-0.pdf>
141141
-/
142142
abbrev LanderParkinSelfridgeConjecture (R : Type*) [Semiring R] (k m n : ℕ) : Prop :=
143143
ExistsEqualSumsOfLikePowersFor R k m n → k ≤ m + n

0 commit comments

Comments
 (0)