bump to nightly-2023-06-17-03

mathlib commit leanprover-community/mathlib@893964f
leanprover-community · Jun 17, 2023 · 253178d · 253178d
1 parent e4403e9
commit 253178d
Show file tree

Hide file tree

Showing 51 changed files with 1,201 additions and 610 deletions.
diff --git a/Archive/All.lean b/Archive/All.lean
@@ -1,17 +1,3 @@
-import Archive.«100-theorems-list».«16AbelRuffini»
-import Archive.«100-theorems-list».«30BallotProblem»
-import Archive.«100-theorems-list».«37SolutionOfCubic»
-import Archive.«100-theorems-list».«42InverseTriangleSum»
-import Archive.«100-theorems-list».«45Partition»
-import Archive.«100-theorems-list».«54Konigsberg»
-import Archive.«100-theorems-list».«57HeronsFormula»
-import Archive.«100-theorems-list».«70PerfectNumbers»
-import Archive.«100-theorems-list».«73AscendingDescendingSequences»
-import Archive.«100-theorems-list».«81SumOfPrimeReciprocalsDiverges»
-import Archive.«100-theorems-list».«82CubingACube»
-import Archive.«100-theorems-list».«83FriendshipGraphs»
-import Archive.«100-theorems-list».«93BirthdayProblem»
-import Archive.«100-theorems-list».«9AreaOfACircle»
 import Archive.Arithcc
 import Archive.Examples.MersennePrimes
 import Archive.Examples.PropEncodable
@@ -52,4 +38,18 @@ import Archive.MiuLanguage.DecisionNec
 import Archive.MiuLanguage.DecisionSuf
 import Archive.OxfordInvariants.«2021summer».Week3P1
 import Archive.Sensitivity
+import Archive.Wiedijk100Theorems.AbelRuffini
+import Archive.Wiedijk100Theorems.AreaOfACircle
+import Archive.Wiedijk100Theorems.AscendingDescendingSequences
+import Archive.Wiedijk100Theorems.BallotProblem
+import Archive.Wiedijk100Theorems.BirthdayProblem
+import Archive.Wiedijk100Theorems.CubingACube
+import Archive.Wiedijk100Theorems.FriendshipGraphs
+import Archive.Wiedijk100Theorems.HeronsFormula
+import Archive.Wiedijk100Theorems.InverseTriangleSum
+import Archive.Wiedijk100Theorems.Konigsberg
+import Archive.Wiedijk100Theorems.Partition
+import Archive.Wiedijk100Theorems.PerfectNumbers
+import Archive.Wiedijk100Theorems.SolutionOfCubic
+import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 
diff --git a/Archive/100-theorems-list/16AbelRuffini.lean → Archive/Wiedijk100Theorems/AbelRuffini.lean b/Archive/100-theorems-list/16AbelRuffini.lean → Archive/Wiedijk100Theorems/AbelRuffini.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 
-! This file was ported from Lean 3 source module «100-theorems-list».«16_abel_ruffini»
-! leanprover-community/mathlib commit 7fdeecc0d03cd40f7a165e6cf00a4d2286db599f
+! This file was ported from Lean 3 source module wiedijk_100_theorems.abel_ruffini
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...ive/100-theorems-list/9AreaOfACircle.lean → ...ive/Wiedijk100Theorems/AreaOfACircle.lean b/...ive/100-theorems-list/9AreaOfACircle.lean → ...ive/Wiedijk100Theorems/AreaOfACircle.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 James Arthur, Benjamin Davidson, Andrew Souther. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Arthur, Benjamin Davidson, Andrew Souther
 
-! This file was ported from Lean 3 source module «100-theorems-list».«9_area_of_a_circle»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.area_of_a_circle
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...-list/73AscendingDescendingSequences.lean → ...heorems/AscendingDescendingSequences.lean b/...-list/73AscendingDescendingSequences.lean → ...heorems/AscendingDescendingSequences.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 
-! This file was ported from Lean 3 source module «100-theorems-list».«73_ascending_descending_sequences»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.ascending_descending_sequences
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...ve/100-theorems-list/30BallotProblem.lean → ...ive/Wiedijk100Theorems/BallotProblem.lean b/...ve/100-theorems-list/30BallotProblem.lean → ...ive/Wiedijk100Theorems/BallotProblem.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Bhavik Mehta, Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Kexing Ying
 
-! This file was ported from Lean 3 source module «100-theorems-list».«30_ballot_problem»
-! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
+! This file was ported from Lean 3 source module wiedijk_100_theorems.ballot_problem
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/.../100-theorems-list/93BirthdayProblem.lean → ...e/Wiedijk100Theorems/BirthdayProblem.lean b/.../100-theorems-list/93BirthdayProblem.lean → ...e/Wiedijk100Theorems/BirthdayProblem.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 
-! This file was ported from Lean 3 source module «100-theorems-list».«93_birthday_problem»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.birthday_problem
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/Archive/100-theorems-list/82CubingACube.lean → Archive/Wiedijk100Theorems/CubingACube.lean b/Archive/100-theorems-list/82CubingACube.lean → Archive/Wiedijk100Theorems/CubingACube.lean
@@ -3,8 +3,8 @@ 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
 
-! This file was ported from Lean 3 source module «100-theorems-list».«82_cubing_a_cube»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.cubing_a_cube
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...100-theorems-list/83FriendshipGraphs.lean → .../Wiedijk100Theorems/FriendshipGraphs.lean b/...100-theorems-list/83FriendshipGraphs.lean → .../Wiedijk100Theorems/FriendshipGraphs.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark, Kyle Miller
 
-! This file was ported from Lean 3 source module «100-theorems-list».«83_friendship_graphs»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.friendship_graphs
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...ve/100-theorems-list/57HeronsFormula.lean → ...ive/Wiedijk100Theorems/HeronsFormula.lean b/...ve/100-theorems-list/57HeronsFormula.lean → ...ive/Wiedijk100Theorems/HeronsFormula.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Matt Kempster. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Matt Kempster
 
-! This file was ported from Lean 3 source module «100-theorems-list».«57_herons_formula»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.herons_formula
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...0-theorems-list/42InverseTriangleSum.lean → ...iedijk100Theorems/InverseTriangleSum.lean b/...0-theorems-list/42InverseTriangleSum.lean → ...iedijk100Theorems/InverseTriangleSum.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jalex Stark, Yury Kudryashov
 
-! This file was ported from Lean 3 source module «100-theorems-list».«42_inverse_triangle_sum»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.inverse_triangle_sum
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/Archive/100-theorems-list/54Konigsberg.lean → Archive/Wiedijk100Theorems/Konigsberg.lean b/Archive/100-theorems-list/54Konigsberg.lean → Archive/Wiedijk100Theorems/Konigsberg.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 
-! This file was ported from Lean 3 source module «100-theorems-list».«54_konigsberg»
-! leanprover-community/mathlib commit af8760ccc4c03bbdff0b140e6f7bd047b0eecbeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.konigsberg
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/Archive/100-theorems-list/45Partition.lean → Archive/Wiedijk100Theorems/Partition.lean b/Archive/100-theorems-list/45Partition.lean → Archive/Wiedijk100Theorems/Partition.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Bhavik Mehta, Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Aaron Anderson
 
-! This file was ported from Lean 3 source module «100-theorems-list».«45_partition»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.partition
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...e/100-theorems-list/70PerfectNumbers.lean → ...ve/Wiedijk100Theorems/PerfectNumbers.lean b/...e/100-theorems-list/70PerfectNumbers.lean → ...ve/Wiedijk100Theorems/PerfectNumbers.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 
-! This file was ported from Lean 3 source module «100-theorems-list».«70_perfect_numbers»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.perfect_numbers
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/.../100-theorems-list/37SolutionOfCubic.lean → ...e/Wiedijk100Theorems/SolutionOfCubic.lean b/.../100-theorems-list/37SolutionOfCubic.lean → ...e/Wiedijk100Theorems/SolutionOfCubic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Jeoff Lee. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeoff Lee
 
-! This file was ported from Lean 3 source module «100-theorems-list».«37_solution_of_cubic»
-! leanprover-community/mathlib commit 7fdeecc0d03cd40f7a165e6cf00a4d2286db599f
+! This file was ported from Lean 3 source module wiedijk_100_theorems.solution_of_cubic
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/...list/81SumOfPrimeReciprocalsDiverges.lean → ...eorems/SumOfPrimeReciprocalsDiverges.lean b/...list/81SumOfPrimeReciprocalsDiverges.lean → ...eorems/SumOfPrimeReciprocalsDiverges.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Manuel Candales. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 
-! This file was ported from Lean 3 source module «100-theorems-list».«81_sum_of_prime_reciprocals_diverges»
-! leanprover-community/mathlib commit 328375597f2c0dd00522d9c2e5a33b6a6128feeb
+! This file was ported from Lean 3 source module wiedijk_100_theorems.sum_of_prime_reciprocals_diverges
+! leanprover-community/mathlib commit 5563b1b49e86e135e8c7b556da5ad2f5ff881cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/Mathbin/Algebra/ContinuedFractions/Computation/Approximations.lean b/Mathbin/Algebra/ContinuedFractions/Computation/Approximations.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.approximations
-! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
+! leanprover-community/mathlib commit cff8231f04dfa33fd8f2f45792eebd862ef30cad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Tactic.SolveByElim
 /-!
 # Approximations for Continued Fraction Computations (`generalized_continued_fraction.of`)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 This file contains useful approximations for the values involved in the continued fractions