Skip to content

Commit 834e516

Browse files
committed
doc: fix Lean 3 namespace in DiophantineApproximation (#39036)
The implementation notes section references the Lean 3 namespace \`real.contfrac_legendre\`, but this was renamed to \`Real.ContfracLegendre\` during the port. This fixes the reference.
1 parent 52e99ad commit 834e516

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/NumberTheory/DiophantineApproximation

Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ in this file, whereas the other, `Real.exists_convs_eq_rat` defined in the file
5555
## Implementation notes
5656
5757
We use the namespace `Real` for the results on real numbers and `Rat` for the results
58-
on rational numbers. We introduce a secondary namespace `real.contfrac_legendre`
58+
on rational numbers. We introduce a secondary namespace `Real.ContfracLegendre`
5959
to separate off a definition and some technical auxiliary lemmas used in the proof
6060
of Legendre's Theorem. For remarks on the proof of Legendre's Theorem, see below.
6161

0 commit comments

Comments
 (0)