[Merged by Bors] - doc(imo*,algebra/continued_fractions/computation): change \minus to -

archive/imo/imo1998_q2.lean

@@ -18,20 +18,20 @@ two judges, their ratings coincide for at most `k` contestants. Prove that `k /
 ## Solution
 The problem asks us to think about triples consisting of a contestant and two judges whose ratings
 agree for that contestant. We thus consider the subset `A ⊆ C × JJ` of all such incidences of
-agreement, where `C` and `J` are the sets of contestants and judges, and `JJ = J × J − {(j, j)}`. We
+agreement, where `C` and `J` are the sets of contestants and judges, and `JJ = J × J - {(j, j)}`. We
 have natural maps: `left : A → C` and `right: A → JJ`. We count the elements of `A` in two ways: as
 the sum of the cardinalities of the fibres of `left` and as the sum of the cardinalities of the
 fibres of `right`. We obtain an upper bound on the cardinality of `A` from the count for `right`,
 and a lower bound from the count for `left`. These two bounds combine to the required result.
 
 First consider the map `right : A → JJ`. Since the size of any fibre over a point in JJ is bounded
-by `k` and since `|JJ| = b^2 - b`, we obtain the upper bound: `|A| ≤ k(b^2−b)`.
+by `k` and since `|JJ| = b^2 - b`, we obtain the upper bound: `|A| ≤ k(b^2-b)`.
 
 Now consider the map `left : A → C`. The fibre over a given contestant `c ∈ C` is the set of
 ordered pairs of (distinct) judges who agree about `c`. We seek to bound the cardinality of this
 fibre from below. Minimum agreement for a contestant occurs when the judges' ratings are split as
 evenly as possible. Since `b` is odd, this occurs when they are divided into groups of size
-`(b−1)/2` and `(b+1)/2`. This corresponds to a fibre of cardinality `(b-1)^2/2` and so we obtain
+`(b-1)/2` and `(b+1)/2`. This corresponds to a fibre of cardinality `(b-1)^2/2` and so we obtain
 the lower bound: `a(b-1)^2/2 ≤ |A|`.
 
 Rearranging gives the result.

archive/imo/imo2005_q4.lean

@@ -9,7 +9,7 @@ import field_theory.finite.basic
 # IMO 2005 Q4
 
 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`.
+`a n = 2 ^ n + 3 ^ n + 6 ^ n - 1`, for `n ≥ 1`.
 
 This is quite an easy problem, in which the key point is a modular arithmetic calculation with
 the sequence `a n` relative to an arbitrary prime.

archive/imo/imo2011_q5.lean

@@ -11,8 +11,8 @@ import data.int.basic
 
 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
-`f(m − n)`.  Prove that, for all integers `m` and `n` with
+`m` and `n`, the difference `f(m) - f(n)` is divisible by
+`f(m - n)`.  Prove that, for all integers `m` and `n` with
 `f(m) ≤ f(n)`, the number `f(n)` is divisible by `f(m)`.
 -/
 

archive/imo/imo2019_q4.lean

@@ -13,7 +13,7 @@ import data.nat.multiplicity
 
 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))
+  k! = (2 ^ n - 1)(2 ^ n - 2)(2 ^ n - 4)···(2 ^ n - 2 ^ (n - 1))
 ```
 We show in this file that this property holds iff `(k, n) = (1, 1) ∨ (k, n) = (3, 2)`.
 

src/algebra/continued_fractions/computation/basic.lean

@@ -14,9 +14,9 @@ import algebra.order.field
 We formalise the standard computation of (regular) continued fractions for linear ordered floor
 fields. The algorithm is rather simple. Here is an outline of the procedure adapted from Wikipedia:
 
-Take a value `v`. We call `⌊v⌋` the *integer part* of `v` and `v − ⌊v⌋` the *fractional part* of
+Take a value `v`. We call `⌊v⌋` the *integer part* of `v` and `v - ⌊v⌋` the *fractional part* of
 `v`.  A continued fraction representation of `v` can then be given by `[⌊v⌋; b₀, b₁, b₂,...]`, where
-`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`.  This
+`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v - ⌊v⌋)`.  This
 process stops when the fractional part hits 0.
 
 In other words: to calculate a continued fraction representation of a number `v`, write down the
@@ -163,7 +163,7 @@ a `continued_fraction` that terminates if and only if `v` is rational (those pro
 added in a future commit).
 
 The continued fraction representation of `v` is given by `[⌊v⌋; b₀, b₁, b₂,...]`, where
-`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`. This
+`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v - ⌊v⌋)`. This
 process stops when the fractional part `v - ⌊v⌋` hits 0 at some step.
 
 The implementation uses `int_fract_pair.stream` to obtain the partial denominators of the continued