chore(*): add mathlib4 synchronization comments (#19238)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.expr` * `algebraic_geometry.morphisms.finite_type` * `algebraic_geometry.morphisms.ring_hom_properties` * `arithcc` * `canonically_ordered_comm_semiring_two_mul` * `char_p_zero_ne_char_zero` * `cyclotomic_105` * `data.matrix.auto` * `direct_sum_is_internal` * `examples.mersenne_primes` * `examples.prop_encodable` * `geometry.manifold.instances.sphere` * `girard` * `homogeneous_prime_not_prime` * `imo.imo1959_q1` * `imo.imo1960_q1` * `imo.imo1962_q1` * `imo.imo1962_q4` * `imo.imo1964_q1` * `imo.imo1969_q1` * `imo.imo1972_q5` * `imo.imo1975_q1` * `imo.imo1977_q6` * `imo.imo1981_q3` * `imo.imo1987_q1` * `imo.imo1988_q6` * `imo.imo1994_q1` * `imo.imo1998_q2` * `imo.imo2001_q2` * `imo.imo2001_q6` * `imo.imo2005_q3` * `imo.imo2005_q4` * `imo.imo2006_q3` * `imo.imo2006_q5` * `imo.imo2008_q2` * `imo.imo2008_q3` * `imo.imo2008_q4` * `imo.imo2011_q3` * `imo.imo2011_q5` * `imo.imo2013_q1` * `imo.imo2013_q5` * `imo.imo2019_q1` * `imo.imo2019_q2` * `imo.imo2019_q4` * `imo.imo2020_q2` * `imo.imo2021_q1` * `linear_order_with_pos_mul_pos_eq_zero` * `map_floor` * `miu_language.basic` * `miu_language.decision_nec` * `miu_language.decision_suf` * `oxford_invariants.2021summer.week3_p1` * `phillips` * `pseudoelement` * `quadratic_form` * `seminorm_lattice_not_distrib` * `sensitivity` * `sorgenfrey_line` * `wiedijk_100_theorems.abel_ruffini` * `wiedijk_100_theorems.area_of_a_circle` * `wiedijk_100_theorems.ascending_descending_sequences` * `wiedijk_100_theorems.ballot_problem` * `wiedijk_100_theorems.birthday_problem` * `wiedijk_100_theorems.cubing_a_cube` * `wiedijk_100_theorems.friendship_graphs` * `wiedijk_100_theorems.herons_formula` * `wiedijk_100_theorems.inverse_triangle_sum` * `wiedijk_100_theorems.konigsberg` * `wiedijk_100_theorems.partition` * `wiedijk_100_theorems.perfect_numbers` * `wiedijk_100_theorems.solution_of_cubic` * `wiedijk_100_theorems.sum_of_prime_reciprocals_diverges` * `zero_divisors_in_add_monoid_algebras`
leanprover-community · Jul 16, 2023 · 08b081e · 08b081e
1 parent 88e6ad4
commit 08b081e
Show file tree

Hide file tree

Showing 73 changed files with 219 additions and 0 deletions.
diff --git a/archive/arithcc.lean b/archive/arithcc.lean
@@ -9,6 +9,9 @@ import tactic.basic
 /-!
 # A compiler for arithmetic expressions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A formalization of the correctness of a compiler from arithmetic expressions to machine language
 described by McCarthy and Painter, which is considered the first proof of compiler correctness.
 

diff --git a/archive/examples/mersenne_primes.lean b/archive/examples/mersenne_primes.lean
@@ -8,6 +8,9 @@ import number_theory.lucas_lehmer
 /-!
 # Explicit Mersenne primes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We run some Lucas-Lehmer tests to prove some Mersenne primes are prime.
 
 See the discussion at the end of [src/number_theory/lucas_lehmer.lean]

diff --git a/archive/examples/prop_encodable.lean b/archive/examples/prop_encodable.lean
@@ -9,6 +9,9 @@ import data.W.basic
 /-!
 # W types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The file `data/W.lean` shows that if `α` is an an encodable fintype and for every `a : α`,
 `β a` is encodable, then `W β` is encodable.
 

diff --git a/archive/imo/imo1959_q1.lean b/archive/imo/imo1959_q1.lean
@@ -10,6 +10,9 @@ import data.nat.prime
 /-!
 # IMO 1959 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every natural number `n`.
 
 Since Lean doesn't have a concept of "irreducible fractions" per se, we just formalize this

diff --git a/archive/imo/imo1960_q1.lean b/archive/imo/imo1960_q1.lean
@@ -9,6 +9,9 @@ import data.nat.digits
 /-!
 # IMO 1960 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine all three-digit numbers $N$ having the property that $N$ is divisible by 11, and
 $\dfrac{N}{11}$ is equal to the sum of the squares of the digits of $N$.
 

diff --git a/archive/imo/imo1962_q1.lean b/archive/imo/imo1962_q1.lean
@@ -9,6 +9,9 @@ import data.nat.digits
 /-!
 # IMO 1962 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Find the smallest natural number $n$ which has the following properties:
 
 (a) Its decimal representation has 6 as the last digit.

diff --git a/archive/imo/imo1962_q4.lean b/archive/imo/imo1962_q4.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.trigonometric.complex
 /-!
 # IMO 1962 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Solve the equation `cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1`.
 
 Since Lean does not have a concept of "simplest form", we just express what is

diff --git a/archive/imo/imo1964_q1.lean b/archive/imo/imo1964_q1.lean
@@ -10,6 +10,9 @@ import data.nat.modeq
 /-!
 # IMO 1964 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 (a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.
 
 (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.

diff --git a/archive/imo/imo1969_q1.lean b/archive/imo/imo1969_q1.lean
@@ -11,6 +11,9 @@ import data.set.finite
 /-!
 # IMO 1969 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that there are infinitely many natural numbers $a$ with the following property:
 the number $z = n^4 + a$ is not prime for any natural number $n$.
 -/

diff --git a/archive/imo/imo1972_q5.lean b/archive/imo/imo1972_q5.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.basic
 /-!
 # IMO 1972 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,
 `f(x + y) + f(x - y) = 2f(x)g(y)`. `f` is not identically zero and `|f(x)| ≤ 1` for all `x`.
 Prove that `|g(x)| ≤ 1` for all `x`.

diff --git a/archive/imo/imo1975_q1.lean b/archive/imo/imo1975_q1.lean
@@ -11,6 +11,9 @@ import algebra.big_operators.ring
 /-!
 # IMO 1975 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `x₁, x₂, ... , xₙ` and `y₁, y₂, ... , yₙ` be two sequences of real numbers, such that
 `x₁ ≥ x₂ ≥ ... ≥ xₙ` and `y₁ ≥ y₂ ≥ ... ≥ yₙ`. Prove that if `z₁, z₂, ... , zₙ` is any permutation
 of `y₁, y₂, ... , yₙ`, then `∑ (xᵢ - yᵢ)^2 ≤ ∑ (xᵢ - zᵢ)^2`

diff --git a/archive/imo/imo1977_q6.lean b/archive/imo/imo1977_q6.lean
@@ -8,6 +8,9 @@ import data.pnat.basic
 /-!
 # IMO 1977 Q6
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Suppose `f : ℕ+ → ℕ+` satisfies `f(f(n)) < f(n + 1)` for all `n`.
 Prove that `f(n) = n` for all `n`.
 

diff --git a/archive/imo/imo1981_q3.lean b/archive/imo/imo1981_q3.lean
@@ -10,6 +10,9 @@ import tactic.linarith
 /-!
 # IMO 1981 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine the maximum value of `m ^ 2 + n ^ 2`, where `m` and `n` are integers in
 `{1, 2, ..., 1981}` and `(n ^ 2 - m * n - m ^ 2) ^ 2 = 1`.
 

diff --git a/archive/imo/imo1987_q1.lean b/archive/imo/imo1987_q1.lean
@@ -11,6 +11,9 @@ import dynamics.fixed_points.basic
 /-!
 # Formalization of IMO 1987, Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $p_{n, k}$ be the number of permutations of a set of cardinality `n ≥ 1` that fix exactly `k`
 elements. Prove that $∑_{k=0}^n k p_{n,k}=n!$.
 

diff --git a/archive/imo/imo1988_q6.lean b/archive/imo/imo1988_q6.lean
@@ -13,6 +13,9 @@ import tactic.wlog
 /-!
 # IMO 1988 Q6 and constant descent Vieta jumping
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Question 6 of IMO1988 is somewhat (in)famous. Several expert problem solvers
 could not tackle the question within the given time limit.
 The problem lead to the introduction of a new proof technique,

diff --git a/archive/imo/imo1994_q1.lean b/archive/imo/imo1994_q1.lean
@@ -14,6 +14,9 @@ import tactic.by_contra
 /-!
 # IMO 1994 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `m` and `n` be two positive integers.
 Let `a₁, a₂, ..., aₘ` be `m` different numbers from the set `{1, 2, ..., n}`
 such that for any two indices `i` and `j` with `1 ≤ i ≤ j ≤ m` and `aᵢ + aⱼ ≤ n`,

diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean
@@ -11,6 +11,9 @@ import tactic.noncomm_ring
 
 /-!
 # IMO 1998 Q2
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 In a competition, there are `a` contestants and `b` judges, where `b ≥ 3` is an odd integer. Each
 judge rates each contestant as either "pass" or "fail". Suppose `k` is a number such that, for any
 two judges, their ratings coincide for at most `k` contestants. Prove that `k / a ≥ (b - 1) / (2b)`.

diff --git a/archive/imo/imo2001_q2.lean b/archive/imo/imo2001_q2.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.pow.real
 /-!
 # IMO 2001 Q2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $a$, $b$, $c$ be positive reals. Prove that
 $$
 \frac{a}{\sqrt{a^2 + 8bc}} +

diff --git a/archive/imo/imo2001_q6.lean b/archive/imo/imo2001_q6.lean
@@ -9,6 +9,9 @@ import tactic.linear_combination
 
 /-!
 # IMO 2001 Q6
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Let $a$, $b$, $c$, $d$ be integers with $a > b > c > d > 0$. Suppose that
 
 $$ a*c + b*d = (a + b - c + d) * (-a + b + c + d). $$

diff --git a/archive/imo/imo2005_q3.lean b/archive/imo/imo2005_q3.lean
@@ -8,6 +8,9 @@ import tactic.positivity
 
 /-!
 # IMO 2005 Q3
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Let `x`, `y` and `z` be positive real numbers such that `xyz ≥ 1`. Prove that:
 `(x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0`
 

diff --git a/archive/imo/imo2005_q4.lean b/archive/imo/imo2005_q4.lean
@@ -8,6 +8,9 @@ import field_theory.finite.basic
 /-!
 # IMO 2005 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Problem: Determine all positive integers relatively prime to all the terms of the infinite sequence
 `a n = 2 ^ n + 3 ^ n + 6 ^ n - 1`, for `n ≥ 1`.
 

diff --git a/archive/imo/imo2006_q3.lean b/archive/imo/imo2006_q3.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.sqrt
 /-!
 # IMO 2006 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine the least real number $M$ such that
 $$
 \left| ab(a^2 - b^2) + bc(b^2 - c^2) + ca(c^2 - a^2) \right|

diff --git a/archive/imo/imo2006_q5.lean b/archive/imo/imo2006_q5.lean
@@ -10,6 +10,9 @@ import dynamics.periodic_pts
 /-!
 # IMO 2006 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $P(x)$ be a polynomial of degree $n>1$ with integer coefficients, and let $k$ be a positive
 integer. Consider the polynomial $Q(x) = P(P(\ldots P(P(x))\ldots))$, where $P$ occurs $k$ times.
 Prove that there are at most $n$ integers $t$ such that $Q(t)=t$.

diff --git a/archive/imo/imo2008_q2.lean b/archive/imo/imo2008_q2.lean
@@ -8,6 +8,9 @@ import data.set.finite
 
 /-!
 # IMO 2008 Q2
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 (a) Prove that
           ```
           x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 ≥ 1

diff --git a/archive/imo/imo2008_q3.lean b/archive/imo/imo2008_q3.lean
@@ -12,6 +12,9 @@ import tactic.linear_combination
 
 /-!
 # IMO 2008 Q3
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Prove that there exist infinitely many positive integers `n` such that `n^2 + 1` has a prime
 divisor which is greater than `2n + √(2n)`.
 

diff --git a/archive/imo/imo2008_q4.lean b/archive/imo/imo2008_q4.lean
@@ -10,6 +10,9 @@ import tactic.linear_combination
 
 /-!
 # IMO 2008 Q4
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Find all functions `f : (0,∞) → (0,∞)` (so, `f` is a function from the positive real
 numbers to the positive real numbers) such that
       ```

diff --git a/archive/imo/imo2011_q3.lean b/archive/imo/imo2011_q3.lean
@@ -9,6 +9,9 @@ import data.real.basic
 /-!
 # IMO 2011 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let f : ℝ → ℝ be a function that satisfies
 
    f(x + y) ≤ y * f(x) + f(f(x))

diff --git a/archive/imo/imo2011_q5.lean b/archive/imo/imo2011_q5.lean
@@ -8,6 +8,9 @@ import data.int.dvd.basic
 /-!
 # IMO 2011 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `f` be a function from the set of integers to the set
 of positive integers.  Suppose that, for any two integers
 `m` and `n`, the difference `f(m) - f(n)` is divisible by

diff --git a/archive/imo/imo2013_q1.lean b/archive/imo/imo2013_q1.lean
@@ -13,6 +13,9 @@ import tactic.field_simp
 /-!
 # IMO 2013 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that for any pair of positive integers k and n, there exist k positive integers
 m₁, m₂, ..., mₖ (not necessarily different) such that
 

diff --git a/archive/imo/imo2013_q5.lean b/archive/imo/imo2013_q5.lean
@@ -12,6 +12,9 @@ import tactic.positivity
 /-!
 # IMO 2013 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `ℚ>₀` be the positive rational numbers. Let `f : ℚ>₀ → ℝ` be a function satisfying
 the conditions
 

diff --git a/archive/imo/imo2019_q1.lean b/archive/imo/imo2019_q1.lean
@@ -8,6 +8,9 @@ import tactic.linarith
 /-!
 # IMO 2019 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine all functions `f : ℤ → ℤ` such that, for all integers `a` and `b`,
 `f(2a) + 2f(b) = f(f(a+b))`.
 

diff --git a/archive/imo/imo2019_q2.lean b/archive/imo/imo2019_q2.lean
@@ -9,6 +9,9 @@ import geometry.euclidean.sphere.second_inter
 /-!
 # IMO 2019 Q2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In triangle `ABC`, point `A₁` lies on side `BC` and point `B₁` lies on side `AC`. Let `P` and
 `Q` be points on segments `AA₁` and `BB₁`, respectively, such that `PQ` is parallel to `AB`.
 Let `P₁` be a point on line `PB₁`, such that `B₁` lies strictly between `P` and `P₁`, and

diff --git a/archive/imo/imo2019_q4.lean b/archive/imo/imo2019_q4.lean
@@ -10,6 +10,9 @@ import data.nat.multiplicity
 /-!
 # IMO 2019 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Find all pairs `(k, n)` of positive integers such that
 ```
   k! = (2 ^ n - 1)(2 ^ n - 2)(2 ^ n - 4)···(2 ^ n - 2 ^ (n - 1))

diff --git a/archive/imo/imo2020_q2.lean b/archive/imo/imo2020_q2.lean
@@ -9,6 +9,9 @@ import analysis.mean_inequalities
 /-!
 # IMO 2020 Q2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The real numbers `a`, `b`, `c`, `d` are such that `a ≥ b ≥ c ≥ d > 0` and `a + b + c + d = 1`.
 Prove that `(a + 2b + 3c + 4d) a^a b^b c^c d^d < 1`.
 

diff --git a/archive/imo/imo2021_q1.lean b/archive/imo/imo2021_q1.lean
@@ -14,6 +14,9 @@ import tactic.ring_exp
 /-!
 # IMO 2021 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `n≥100` be an integer. Ivan writes the numbers `n, n+1,..., 2n` each on different cards.
 He then shuffles these `n+1` cards, and divides them into two piles. Prove that at least one
 of the piles contains two cards such that the sum of their numbers is a perfect square.

diff --git a/archive/miu_language/basic.lean b/archive/miu_language/basic.lean
@@ -8,6 +8,9 @@ import tactic.linarith
 /-!
 # An MIU Decision Procedure in Lean
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The [MIU formal system](https://en.wikipedia.org/wiki/MU_puzzle) was introduced by Douglas
 Hofstadter in the first chapter of his 1979 book,
 [Gödel, Escher, Bach](https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach).

diff --git a/archive/miu_language/decision_nec.lean b/archive/miu_language/decision_nec.lean
@@ -11,6 +11,9 @@ import tactic.ring
 /-!
 # Decision procedure: necessary condition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce a condition `decstr` and show that if a string `en` is `derivable`, then `decstr en`
 holds.
 

diff --git a/archive/miu_language/decision_suf.lean b/archive/miu_language/decision_suf.lean
@@ -9,6 +9,9 @@ import tactic.linarith
 /-!
 # Decision procedure - sufficient condition and decidability
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We give a sufficient condition for a string to be derivable in the MIU language. Together with the
 necessary condition, we use this to prove that `derivable` is an instance of `decidable_pred`.
 

diff --git a/archive/oxford_invariants/2021summer/week3_p1.lean b/archive/oxford_invariants/2021summer/week3_p1.lean
@@ -11,6 +11,9 @@ import data.rat.cast
 /-!
 # The Oxford Invariants Puzzle Challenges - Summer 2021, Week 3, Problem 1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Original statement
 
 Let `n ≥ 3`, `a₁, ..., aₙ` be strictly positive integers such that `aᵢ ∣ aᵢ₋₁ + aᵢ₊₁` for

diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean
@@ -15,6 +15,9 @@ import data.real.sqrt
 /-!
 # Huang's sensitivity theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A formalization of Hao Huang's sensitivity theorem: in the hypercube of
 dimension n ≥ 1, if one colors more than half the vertices then at least one
 vertex has at least √n colored neighbors.