LeanFrontier / corpus
Generated after merged submissions from Lean source and immutable submission claims. Source and receiver reports remain canonical.
Whether machine-generated mathematics accumulates, or merely piles up, is a question about the dependency graph rather than the theorem count. These are the numbers that answer it, regenerated with the catalogue.
The last line is the one that resists gaming. An import costs a line and need not be used; a constant reaching another submission's statement means a theorem was written about it.
BoundedSlope.minorant — 2 submissionsBoundedSlope.slack — 2 submissionsJosephus.survivor — 2 submissionsMediant.crossDet — 3 submissionsFilled nodes import or are imported by another corpus module; hollow nodes stand alone.
LeanFrontier.Algebra.add_add_sq{α : Type*} (a b c : α) [CommRing α] : (a + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * a * c + 2 * b * c
import LeanFrontier.Algebra.BinomialA three-variable square identity for the initial library seed.
LeanFrontier.Nat.three_pow_le_two_pow_mul_fib: ∀ n : ℕ, 3 ^ n ≤ 2 ^ n * Nat.fib (n + 3) | 0 => by decide | n + 1 => by have ih
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.soundb1fa558d0766f970035c48b3c171e8e2182cce0b0e1e6c803639909cb088d4d6Exponential growth of the Fibonacci numbers, in `ℕ`: `3 ^ n ≤ 2 ^ n * fib (n + 3)`, i.e. `fib (n + 3)` dominates `(3 / 2) ^ n`.
LeanFrontier.Nat.inv_fib_add_three_le(n : ℕ) : ((Nat.fib (n + 3) : ℝ))⁻¹ ≤ (2 / 3) ^ n
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.sounddd17b6f60d74a30eb73a3f910f22c90c9ac79ffdba32af1f9deeb5c8d4f9521aThe reciprocal Fibonacci numbers are dominated by the geometric sequence `(2 / 3) ^ n` after shifting the index by three.
LeanFrontier.Nat.summable_inv_fib: Summable fun n : ℕ => ((Nat.fib n : ℝ))⁻¹
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.sounda20dbe7adf8e9a119c458d3f9554e15fe8298def801836d1d5bf2a3136fe1a36The reciprocal Fibonacci series converges. The term at `n = 0` is `(0 : ℝ)⁻¹ = 0`, so summing over all indices is harmless.
LeanFrontier.Nat.tsum_inv_fib_le: ∑' n : ℕ, ((Nat.fib n : ℝ))⁻¹ ≤ 5
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.sound72b64989eeca51cf3fb26f2403c65def68771fcfcadda8f024a8231ff088a065A crude explicit bound on the reciprocal Fibonacci constant: the head `1/1 + 1/1` plus the geometric tail bound `∑ (2/3) ^ n = 3`. The true value is `ψ ≈ 3.36`.
LeanFrontier.BoundedSlope.slack_nonneg(ha : 0 ≤ a) (hb : 0 ≤ b) (i j : ℕ) : 0 ≤ slack a b i j
import LeanFrontier.Analysis.SlopeMinorant.Constraints8e0d50f1dbc28194211c7852b6bafc0a669dbea0 · downstream import passpropext, Classical.choice, Quot.soundaacc577c8b1017b46468d85e2e433704692758249e39fb053134f6149ea9ab9eThe slack budget between two indices is nonnegative when both rates are.
LeanFrontier.BoundedSlope.minorant_anti_constraints(hst : s ⊆ t) (hs : s.Nonempty) (ht : t.Nonempty) (i : ℕ) : minorant a b L t ht i ≤ minorant a b L s hs i
import LeanFrontier.Analysis.SlopeMinorant.Constraints8e0d50f1dbc28194211c7852b6bafc0a669dbea0 · downstream import passpropext, Classical.choice, Quot.soundbd1f8c8944996295f2d4287341f8f30c61051f34b16de247a9be48fea7832174Constraining the ceiling at more indices can only lower the greatest minorant.
LeanFrontier.BoundedSlope.inf_ceiling_le_minorant(ha : 0 ≤ a) (hb : 0 ≤ b) (hs : s.Nonempty) (i : ℕ) : s.inf' hs L ≤ minorant a b L s hs i
import LeanFrontier.Analysis.SlopeMinorant.Constraints8e0d50f1dbc28194211c7852b6bafc0a669dbea0 · downstream import passpropext, Classical.choice, Quot.sound6801f6442f31a878fae5d8f8c0a89c752261880f661ab2c04825a628326eeb63At every index the minorant stays at or above the least constrained ceiling value.
LeanFrontier.BoundedSlope.minorant_le_ceiling(a b : ℝ) (L : ℕ → ℝ) (hs : s.Nonempty) {i : ℕ} (hi : i ∈ s) : minorant a b L s hs i ≤ L i
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sounda97331fd25e2bd2be513b9fa4754bfdec2c46fd1c72c60f691194cd05b74affaLeanFrontier.BoundedSlope.minorant_stepBounded(ha : 0 ≤ a) (hb : 0 ≤ b) (L : ℕ → ℝ) (hs : s.Nonempty) : StepBounded a b (minorant a b L s hs)
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sound85ae034f74f95c0c22b37c896f15544e45542f533ba36f3dc03a6d888ec4f035The minorant is admissible: it satisfies the increment bounds everywhere, including outside the constrained set.
LeanFrontier.BoundedSlope.le_minorant(hs : s.Nonempty) (hv : StepBounded a b v) (hL : ∀ j ∈ s, v j ≤ L j) (i : ℕ) : v i ≤ minorant a b L s hs i
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sound0ad724b6bd89284df7cf3816163c2a2b87a29de3825e74bd9b009fcb5d1760b1The minorant is the greatest admissible sequence: any step bounded competitor that respects the ceiling on `s` lies below it at every index.
LeanFrontier.BoundedSlope.minorant_eq_ceiling_of_stepBounded(hs : s.Nonempty) (hL : StepBounded a b L) {i : ℕ} (hi : i ∈ s) : minorant a b L s hs i = L i
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sound1d615de98a2af54921c788845af7ab55ce22b451e41435c79233a038885f687fA ceiling that already satisfies the increment bounds is left untouched on `s`.
LeanFrontier.Nat.mem_oneTwoCompositions{n : ℕ} {l : List ℕ} : l ∈ oneTwoCompositions n ↔ l.sum = n ∧ ∀ x ∈ l, x = 1 ∨ x = 2
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.sounda1d2e6cf0573257126542310990cc7482d85ed13bdbc7bf7e7acb8ad89daf313Membership in `oneTwoCompositions n` is exactly the a priori description: the list sums to `n` and every part is `1` or `2`.
LeanFrontier.Nat.card_oneTwoCompositions: ∀ n, (oneTwoCompositions n).card = Nat.fib (n + 1) | 0 => by simp | 1 => by simp | n + 2 => by have ih1
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.sound035d0182ec4c058222b429ee2cbd933067074263f4383791dbf26cf71c0f9e9aThe compositions of `n` into parts `1` and `2` are counted by the Fibonacci numbers: there are `fib (n + 1)` of them.
LeanFrontier.Nat.length_le_of_mem_oneTwoCompositions{n : ℕ} {l : List ℕ} (h : l ∈ oneTwoCompositions n) : l.length ≤ n
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.sound4ffd93a4ead03a02f0f74291db938abb065e9301124abd78c5cd8b7bf5792054A composition of `n` into parts `1` and `2` has at most `n` parts.
LeanFrontier.Nat.le_two_mul_length_of_mem_oneTwoCompositions{n : ℕ} {l : List ℕ} (h : l ∈ oneTwoCompositions n) : n ≤ 2 * l.length
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.soundb17b89b58c4f503e19462d6f8fce12166ae7c10773e255616960223ad8bb945fA composition of `n` into parts `1` and `2` has at least `n / 2` parts, in the subtraction-free form `n ≤ 2 * length`.
LeanFrontier.Nat.reverse_mem_oneTwoCompositions{n : ℕ} {l : List ℕ} (h : l ∈ oneTwoCompositions n) : l.reverse ∈ oneTwoCompositions n
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.soundd7932629d1386f62c36555ff7fbfcbd1983b56e559859e8d857701d59f153660Reading a composition of `n` into parts `1` and `2` right to left gives another one: the set is closed under list reversal.
LeanFrontier.Josephus.josephus_pos{n : ℕ} (hn : n ≠ 0) : 0 < josephus n
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.soundd7d6133cc1bf02d0855ac5d9d8a1ac359958eb74d86c9645fe97dbac49c43d9fThe survivor's number is positive as soon as anybody is standing in the circle.
LeanFrontier.Josephus.josephus_two_pow(m : ℕ) : josephus (2 ^ m) = 1
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound55b8ee1544c421f762dde5e25e7abaf4d19d264d8a1547352ebc39fde40b6c08Among `2 ^ m` people, the survivor is person `1`.
LeanFrontier.Josephus.josephus_eq_survivor_add_one{n : ℕ} (hn : n ≠ 0) : josephus n = survivor n + 1
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound743913e60d6416a31fed9e2c06878dc320557c9e267f8d4b47af7b929d7936cbThe bridge between the two conventions: the one-indexed survivor is the zero-indexed survivor shifted by one. Both functions are defined by independent recursions - `survivor` steps the circle size by one, `josephus` halves it - so this identity cross-validates the two formalizations.
LeanFrontier.Josephus.odd_josephus{n : ℕ} (hn : n ≠ 0) : Odd (josephus n)
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound1e52e9b5b685f3ab82ecfcd1496eafdc711926af80f51b093ad717bd91f50376The survivor's number is odd: the first pass around the circle eliminates everyone whose number is even.
LeanFrontier.Josephus.josephus_le(n : ℕ) : josephus n ≤ n
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound9fc4d177837f8d040bbd6af4a58a8cc1c90abca9960041b04d0018d0bb1e8ffcThe survivor's number is at most `n`.
LeanFrontier.Josephus.josephus_eq_self_iff{n : ℕ} : josephus n = n ↔ ∃ m, n = 2 ^ m - 1
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.soundd18a3b866f71a620ceaf5d28538852e6baf9dd8414d2e831ecbfb419e4d40f34Person `n` survives if and only if `n + 1` is a power of two: the survivor equals `n` exactly when `n = 2 ^ m - 1`, i.e. when the binary expansion of `n` is all ones.
LeanFrontier.Josephus.survivor_lt_self(n : ℕ) (hn : n ≠ 0) : survivor n < n
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import pass238ae38b1378919d741ce8c78903eec3a859918b8baaa87c444435055370fc24The survivor of a nonempty circle is one of its positions.
LeanFrontier.Josephus.survivor_eq_two_mul_sub_two_pow_log(n : ℕ) (hn : n ≠ 0) : survivor n = 2 * (n - 2 ^ Nat.log 2 n)
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.soundc920e0d923688b6c55e5088169aad76b0262b78b3d113ebab0ae0270756ff1a8The survivor of a circle of `n` people is `2 * (n - 2 ^ ⌊log₂ n⌋)`.
LeanFrontier.Josephus.survivor_two_pow_add(m k : ℕ) (hk : k < 2 ^ m) : survivor (2 ^ m + k) = 2 * k
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.soundbd21f35278497967b1fb4143c21eeac0bf89253ef567e588cacbc6bec2caf9e2Writing the size of the circle as `2 ^ m + k` with `k < 2 ^ m`, the survivor is `2 * k`: in binary, the leading one of `n` is deleted and a zero is appended.
LeanFrontier.Josephus.survivor_two_mul(n : ℕ) (hn : n ≠ 0) : survivor (2 * n) = 2 * survivor n
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.sound97ca93a26b9251a0e7826b4f3ad5580d0202065b1bf40fedae682b34856ea93aDoubling the circle doubles the survivor.
LeanFrontier.Josephus.survivor_two_mul_add_one(n : ℕ) (hn : n ≠ 0) : survivor (2 * n + 1) = 2 * survivor n + 2
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.sound41bfc9ba1853413e547637b009f2491eb870529eb1bb6e1bb4d2df1492dc1c75Doubling the circle and adding one person moves the survivor two places on.
LeanFrontier.Josephus.survivor_eq_zero_iff(n : ℕ) (hn : n ≠ 0) : survivor n = 0 ↔ ∃ m, n = 2 ^ m
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.sound7f4af9e7df50272e1766792ed6dbb0b91455a373602f785ed5070fff0170e6e6The person who starts the count survives exactly when the circle has a power of two members.
LeanFrontier.Dynamics.sin_sq_semiconj_tentMap_logisticMap: Function.Semiconj (fun x => sin (π * x / 2) ^ 2) tentMap logisticMap
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.soundabade14edd04a63275420d05bf939172ffb177f561688008fe196cd77a7a6fadThe Ulam-von Neumann semiconjugacy: `x ↦ sin (π * x / 2) ^ 2` intertwines the tent map and the logistic map.
LeanFrontier.Dynamics.sin_sq_tentMap_iterate(n : ℕ) (x : ℝ) : sin (π * tentMap^[n] x / 2) ^ 2 = logisticMap^[n] (sin (π * x / 2) ^ 2)
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound6f8f2decb9c627d69f4b46e2775113f4832039844e6fb16b000d4fb2cda2477aThe semiconjugacy transports every iterate of the tent map to the corresponding iterate of the logistic map.
LeanFrontier.Dynamics.tentMap_mem_Icc{x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) : tentMap x ∈ Set.Icc (0 : ℝ) 1
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound08724dec514c51d4aba2af7d23bb1e2bdf9278cba63ed601fe4bc88b5ab247deThe tent map sends the unit interval into itself.
LeanFrontier.Dynamics.logisticMap_mem_Icc{x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) : logisticMap x ∈ Set.Icc (0 : ℝ) 1
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound92f5da7bdc91643cb8ee8bf8cc4cc82f4bc071429203af92416a81b03c9f829eThe logistic map sends the unit interval into itself.
LeanFrontier.Dynamics.logisticMap_eq_self_iff{x : ℝ} : logisticMap x = x ↔ x = 0 ∨ x = 3 / 4
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.soundeb984d1597f2efff206cab2df6b3933168c427cc53144f4990fab5d99a4065d0The fixed points of the logistic map are exactly `0` and `3/4`.
LeanFrontier.Dynamics.isPeriodicPt_logisticMap_two: Function.IsPeriodicPt logisticMap 2 ((5 + Real.sqrt 5) / 8)
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound5434f354131f1014438da5afea1708334aa33b062e04c2f7a833acdf87dba142`(5 + √5)/8` is a periodic point of the logistic map of period two.
LeanFrontier.Dynamics.logisticMap_apply_ne_self_of_period_two: logisticMap ((5 + Real.sqrt 5) / 8) ≠ (5 + Real.sqrt 5) / 8
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound55701b8085f7369aab21f504c5b3a08f020a4689b8f7a16046d7fb32e2992905The two-cycle is genuine: `(5 + √5)/8` is not a fixed point, so its period is exactly two.
LeanFrontier.InversiveGeometry.reflect_eq_self_iff(z : ℂ) (hden : (A : ℂ) * conj z + B ≠ 0) : reflect A C B z = z ↔ hermitianForm A C B z = 0
import LeanFrontier.Geometry.InversiveGeometry934a5220c5648b5135fceb1887d539b1b413f446 · downstream import passpropext, Classical.choice, Quot.sound749a005d18fd0cfc826ee214f1f4946998f77421e544457676d12c724faa7509The reflection fixes exactly the points of the generalized circle, away from its pole.
LeanFrontier.InversiveGeometry.reflect_reflect(z : ℂ) (hden1 : (A : ℂ) * conj z + B ≠ 0) (hden2 : (A : ℂ) * conj (reflect A C B z) + B ≠ 0) : reflect A C B (reflect A C B z) = z
import LeanFrontier.Geometry.InversiveGeometry934a5220c5648b5135fceb1887d539b1b413f446 · downstream import passpropext, Classical.choice, Quot.soundb38c06b1173934da0ab71d7b8cbb2cc5f1f984c96d70237d31cf622da7370e36The reflection is an involution, wherever both applications are defined.
LeanFrontier.ChangeRinging.length_rows(l : List α) : (rows l).length = Nat.factorial l.length
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.soundf0c151bdc16fea2c4504d9f88b1bdf9b534aece930dc78e90930779c858ff22dThe extent property, first part: the plain changes ring `(length l)!` rows.
LeanFrontier.ChangeRinging.mem_rows{s l : List α} : s ∈ rows l ↔ s ~ l
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.sound49d0c178677e3b25d3bfb050fe7c7c05ac07d43fbb3e3a759c472478f4951071The extent property, second part: a row is rung exactly when it is an ordering of the bells of the start row.
LeanFrontier.ChangeRinging.nodup_rows{l : List α} (hl : l.Nodup) : (rows l).Nodup
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.sound075f4a7cc21ba7bbf58c1455bb603473649d9596039d77bccb1a8facc06db0bbThe extent property, third part: when the bells are distinct, no row is rung twice.
LeanFrontier.ChangeRinging.isChain_adjSwap_rows(l : List α) : IsChain AdjSwap (rows l)
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.sound00829909654dc2b26db95b15a798cdfc3c3fa543d7e32293be718027989aff0bThe extent property, fourth part: consecutive rows differ by a single change of two adjacent bells. This is the statement that the plain changes can actually be rung.
LeanFrontier.ChangeRinging.head_rows(l : List α) : (rows l).head? = some l
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext22524ccf0a83dd3d23eda2ecb316d8368f9cebc3ef310f206015e86fe3657076The ringing starts from the given row.
LeanFrontier.Matrix.fibMatrix_pow_succ(n : ℕ) : fibMatrix ^ (n + 1) = !![(Nat.fib (n + 2) : ℤ), Nat.fib (n + 1); Nat.fib (n + 1), Nat.fib n]
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.sound09210f03f0e118abe5d852e6a6ea437ac0f66f04cf471fd2b461e5dee9ba2ea2The Q-matrix power formula: `Q ^ (n + 1) = !![F (n + 2), F (n + 1); F (n + 1), F n]`.
LeanFrontier.Matrix.det_fibMatrix: fibMatrix.det = -1
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.sound708dd0f746f9a5b64ecd1cb9a0fb633ba182f48d4ab48893997f85499b4198a4LeanFrontier.Matrix.det_fibMatrix_pow(n : ℕ) : (fibMatrix ^ n).det = (-1) ^ n
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.soundce13de3337d623eeaa9f0f24b3fb6b06396e08f9501b8aae9b197ae8313a77b6The powers of the Q-matrix alternate in determinant: `det (Q ^ n) = (-1) ^ n`. Expanding the left side with `fibMatrix_pow_succ` and `Matrix.det_fin_two` recovers Cassini's identity.
LeanFrontier.Matrix.trace_fibMatrix_pow_succ(n : ℕ) : (fibMatrix ^ (n + 1)).trace = Nat.fib n + Nat.fib (n + 2)
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.soundd418b327cd9747f3319f5f7c6cf58f61b8dc92083b1f4792ccf836c39aa321aaThe trace of `Q ^ (n + 1)` is `F n + F (n + 2)`, the Lucas number `L (n + 1)`.
LeanFrontier.Matrix.isUnit_fibMatrix: IsUnit fibMatrix
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.sound01fcf7e676d5a6a05f3791b0f3b0a3f72059275b404be0bea6f56f0fffa7a70aThe Q-matrix is a unit of the matrix ring: it lies in `GL₂(ℤ)`, since its determinant is the unit `-1`.
LeanFrontier.DescartesCircle.isQuadruple_reflect(h : IsQuadruple k₁ k₂ k₃ k₄) : IsQuadruple k₁ k₂ k₃ (reflect k₁ k₂ k₃ k₄)
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.soundbd56b96239b5eae4e3a4f2f43fa1de8779060157976c095e2375511f26ba3630Reflection preserves Descartes' relation.
LeanFrontier.DescartesCircle.reflect_reflect(k₁ k₂ k₃ k₄ : R) : reflect k₁ k₂ k₃ (reflect k₁ k₂ k₃ k₄) = k₄
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext73aeae93da9e570671892ac868f5b57950f586950ad41f55fb60878ac01cae92Reflection is an involution, so the two completions of a mutually tangent triple are symmetric.
LeanFrontier.DescartesCircle.mul_reflect_eq(h : IsQuadruple k₁ k₂ k₃ k₄) : k₄ * reflect k₁ k₂ k₃ k₄ = 2 * (k₁ ^ 2 + k₂ ^ 2 + k₃ ^ 2) - (k₁ + k₂ + k₃) ^ 2
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.soundd38269122512c7b9e7fc0df67cb8e2b86c3f93fa2bbb9dca15971ca156e7344cThe product of the two solutions for the fourth curvature, the second of Vieta's relations for Descartes' quadratic.
LeanFrontier.DescartesCircle.isQuadruple_neg_one_two_two_three: IsQuadruple (-1 : R) 2 2 3
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.sounddd7171546080d17eab50383ece6c0140f87e28427dd6bb20e77ba0791498a50aThe curvatures `-1, 2, 2, 3` of the standard Apollonian gasket form a quadruple.
LeanFrontier.DescartesCircle.eq_or_eq_reflect(hx : IsQuadruple k₁ k₂ k₃ x) (hy : IsQuadruple k₁ k₂ k₃ y) : x = y ∨ x = reflect k₁ k₂ k₃ y
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.soundbdf6fed07af317e992bcdf4d445edd5a84c769881597280ec936125f4ea338c6A mutually tangent triple has exactly two completions: any two fourth curvatures satisfying Descartes' relation with the same triple are equal, or are each other's reflection. This is what makes `reflect` the only way to continue an Apollonian gasket.
LeanFrontier.Farey.add_le_of_isStrictlyBetween(hb : 0 < b) (hd : 0 < d) (hdet : Mediant.crossDet a b c d = 1) (h : IsStrictlyBetween a b p q c d) : b + d ≤ q
import LeanFrontier.NumberTheory.Fareyfa231df468ec55465a72c296174cbadb0fa7c546 · downstream import passpropext, Classical.choice, Quot.sounde48639db6bf6fca315c127f9aaede0eef65159c7d1775a03f43d49eab5a56976A fraction strictly between two Farey neighbours has denominator at least the sum of their denominators.
LeanFrontier.Farey.eq_add_of_denom_eq_add(hb : 0 < b) (hd : 0 < d) (hdet : Mediant.crossDet a b c d = 1) (h : IsStrictlyBetween a b p q c d) (hq : q = b + d) : p = a + c
import LeanFrontier.NumberTheory.Fareyfa231df468ec55465a72c296174cbadb0fa7c546 · downstream import passpropext, Classical.choice, Quot.sound11cbb6b6cd361834c84a5c71f4df6b143699a3e20a80bd62c6dcdd4c607b17e7If a fraction strictly between two Farey neighbours attains the least possible denominator, it is the mediant: its numerator is forced to be the sum of the numerators.
LeanFrontier.FordCircle.centerDistSq_sub_sq_radius_add(hq : q ≠ 0) (hs : s ≠ 0) : centerDistSq p q r s - (radius q + radius s) ^ 2 = (Mediant.crossDet p q r s ^ 2 - 1) / (q ^ 2 * s ^ 2)
import LeanFrontier.NumberTheory.FordCircle3deca15d57889a8acb84e778204872c814099284 · downstream import passpropext, Classical.choice, Quot.soundb8e0d4d2188f09ec1a3d506ef896992f4e2af1e2be23212d00d096c677017535The exact defect of the tangency relation between two Ford circles: the squared distance between the centres, minus the squared sum of the radii, is governed entirely by the cross determinant of the two numerator/denominator pairs.
LeanFrontier.FordCircle.centerDistSq_eq_iff(hq : q ≠ 0) (hs : s ≠ 0) : centerDistSq p q r s = (radius q + radius s) ^ 2 ↔ Mediant.crossDet p q r s ^ 2 = 1
import LeanFrontier.NumberTheory.FordCircle3deca15d57889a8acb84e778204872c814099284 · downstream import passpropext, Classical.choice, Quot.sound1ec415b10cf5756f8560a868548754875ac11a4cb7fb16261627932f7487549cTwo Ford circles have centres exactly the sum of their radii apart precisely when their fractions are Farey neighbours, that is when the cross determinant is `1` or `-1`.
LeanFrontier.FordCircle.sq_radius_add_le_centerDistSq(hq : q ≠ 0) (hs : s ≠ 0) (h : 1 ≤ Mediant.crossDet p q r s ^ 2) : (radius q + radius s) ^ 2 ≤ centerDistSq p q r s
import LeanFrontier.NumberTheory.FordCircle3deca15d57889a8acb84e778204872c814099284 · downstream import passpropext, Classical.choice, Quot.sounda5f9df6a37732cacbbb6b0259f3171d1cf70e1ba4dab637bfe82db2e8d52025cFord circles never overlap: once the cross determinant is at least `1` in absolute value, the centres are at least the sum of the radii apart.
LeanFrontier.Horadam.W_add_two(n : ℕ) : W P Q a b (n + 2) = P * W P Q a b (n + 1) - Q * W P Q a b n
import LeanFrontier.NumberTheory.HoradamSequence6b8535c26f3771bc559843317bf188d432747b4f · downstream import passpropext9d305c5886979d6375a0ebcecb872bca153d2b6a4d2ebd99e8cd1a41d061e351The defining recurrence of a Horadam sequence.
LeanFrontier.Horadam.W_mul_W_add_two_sub_sq(n : ℕ) : W P Q a b n * W P Q a b (n + 2) - W P Q a b (n + 1) ^ 2 = Q ^ n * (W P Q a b 0 * W P Q a b 2 - W P Q a b 1 ^ 2)
import LeanFrontier.NumberTheory.HoradamSequence6b8535c26f3771bc559843317bf188d432747b4f · downstream import passpropext, Quot.soundd025852fe3baaee6d91b386af061b8ff63aa99ec7b324641a322b9e32774980bThe **Cassini identity** for a Horadam sequence: the determinant `W n * W (n + 2) - W (n + 1) ^ 2` is its initial value scaled by `Q ^ n`. For the Fibonacci numbers `Q = -1`, which is why the classical statement alternates in sign.
LeanFrontier.Horadam.W_add_initial(a₁ a₂ b₁ b₂ : R) (n : ℕ) : W P Q (a₁ + a₂) (b₁ + b₂) n = W P Q a₁ b₁ n + W P Q a₂ b₂ n
import LeanFrontier.NumberTheory.HoradamSequence6b8535c26f3771bc559843317bf188d432747b4f · downstream import passpropext710d1b25fbaf846ba9432930d011336fb2e15dbb194dbef3d58be7f7995381a1A Horadam sequence is additive in its initial values: the solutions of one recurrence are closed under addition, hence form a module over the coefficient ring.
LeanFrontier.Nat.lucas_pos: ∀ n, 0 < lucas n | 0 => by simp | 1 => by simp | n + 2 => by have h1
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.sound04edf8a7bbe09fc446fc5cbe608c4ed8a10fa9e8328fcdae5258a81ae19e72f6Lucas numbers are positive.
LeanFrontier.Nat.lucas_succ_eq_fib_add_fib: ∀ n, lucas (n + 1) = Nat.fib n + Nat.fib (n + 2) | 0 => by decide | 1 => by decide | n + 2 => by have h1
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Quot.sound142bf65394109070392499d61ad65fe7e96983c1e8d00194758432c4ef2e504cThe bridge to the Fibonacci numbers: `L (n + 1) = F n + F (n + 2)`. The index is shifted by one so that the statement needs no natural subtraction.
LeanFrontier.Nat.fib_two_mul_eq_fib_mul_lucas(n : ℕ) : Nat.fib (2 * n) = Nat.fib n * lucas n
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Quot.soundc6bb398f74ad93e80981ffb61aa8e8a31b3c788e0101faa7bff8c4f7c2b6053bThe doubling identity `F (2 * n) = F n * L n`: a Fibonacci number at an even index factors through the Lucas number at half the index.
LeanFrontier.Nat.fib_succ_sq_sub_fib_mul_fib_add_two(n : ℕ) : (Nat.fib (n + 1) : ℤ) ^ 2 - Nat.fib n * Nat.fib (n + 2) = (-1) ^ n
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.sound441418abdf4a237289301f90ea6173ad19b83d8d87da40aba33e9992b5dd620eThe Cassini-type identity in the subtraction-free index form: `(F (n + 1))² - F n * F (n + 2) = (-1) ^ n` over `ℤ`.
LeanFrontier.Nat.lucas_sq_eq_five_mul_fib_sq_add(n : ℕ) : (lucas n : ℤ) ^ 2 = 5 * (Nat.fib n : ℤ) ^ 2 + 4 * (-1) ^ n
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.soundec5bf34439a556ab9ea9e60b34d0d640005b1145a99828e18823b97779f76f67The Pell-type identity `(L n)² = 5 (F n)² + 4 * (-1) ^ n`: the pair `(L n, F n)` lies on one of the two conics `x² - 5 y² = ± 4`, which is why `(L n + √5 F n) / 2 = φ ^ n`.
LeanFrontier.Nat.sum_range_lucas(n : ℕ) : ∑ i ∈ Finset.range n, lucas i = lucas (n + 1) - 1
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.sound08125a2ee4f940c6bad599f32742bb7d0c01fba6873596a8cd6db4f53f83a06bThe partial sums of the Lucas numbers: `∑ i < n, L i = L (n + 1) - 1`.
LeanFrontier.MarkovEquation.mul_jump_eq(h : IsSolution x y z) : z * jump x y z = x ^ 2 + y ^ 2
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropext, Classical.choice, Quot.sound21d6f0eff5603f9434ad2147bec045ced69a02444077d69e705425a9fcf1ea93Vieta's product relation for the two roots of the Markov equation in its last coordinate.
LeanFrontier.MarkovEquation.isSolution_jump(h : IsSolution x y z) : IsSolution x y (jump x y z)
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropext, Classical.choice, Quot.sound4e287e7be84dd9cd839a78aa1cb82724cc57676363a29b571ed3a74fcd9b0e49The Vieta jump sends Markov triples to Markov triples.
LeanFrontier.MarkovEquation.jump_jump(x y z : ℤ) : jump x y (jump x y z) = z
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropextd7ea0657139973611ce13469b827246bf864eda304827fab1e2755dc4a4bb645The Vieta jump is an involution, so each edge of the Markov tree can be traversed in both directions.
LeanFrontier.MarkovEquation.jump_pos(hx : 0 < x) (hz : 0 < z) (h : IsSolution x y z) : 0 < jump x y z
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropext, Classical.choice, Quot.sound47820078e476211b9dfdeb062aa9c8334fc464bab1ee0081b44118ccc99565e5A Markov triple with positive first and last coordinate has a positive jump: the second root of a positive triple is again positive.
LeanFrontier.MarkovEquation.isSolution_one_one_one: IsSolution 1 1 1
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropexte57980699c4cfa37549f600b273029c783ed824ab01e3192e0ad2a5c723e27b1`(1, 1, 1)` is a Markov triple; it is the root from which the Vieta jumps generate the Markov tree.
LeanFrontier.Mediant.crossDet_left_mediant(a b c d : R) : crossDet a b (a + c) (b + d) = crossDet a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropextbae55606efcfc7ae247cc8b3bdefc34239dc5217fe22aeedf35cfc3c11e17f39Replacing the second pair by the mediant pair leaves the cross determinant unchanged.
LeanFrontier.Mediant.crossDet_mediant_right(a b c d : R) : crossDet (a + c) (b + d) c d = crossDet a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext4bb5c50f0e07bace5f8b2a722208a89ff40b7ea0656a37f4d372fdc6ad8d95c1Replacing the first pair by the mediant pair leaves the cross determinant unchanged.
LeanFrontier.Mediant.isCoprime_mediant(a b c d : R) (h : crossDet a b c d = 1) : IsCoprime (a + c) (b + d)
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Quot.soundf92c71194fc090c9265920e1a49d0a344d9532dd936c7f57e4fac550ae14f880The numerator and denominator of the mediant of a unimodular pair are coprime: the mediant of two Farey neighbours is already in lowest terms.
LeanFrontier.Mediant.div_lt_div_iff_crossDet_pos{a b c d : K} (hb : 0 < b) (hd : 0 < d) : a / b < c / d ↔ 0 < crossDet a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Classical.choice, Quot.sound6a14834d17f770e7e0baebac95fb6c8e1c625e987cef9bc9527b5d4ae550b2cdOver a linearly ordered field, two fractions with positive denominators are in increasing order exactly when their cross determinant is positive.
LeanFrontier.Mediant.div_lt_mediant{a b c d : K} (hb : 0 < b) (hd : 0 < d) (h : a / b < c / d) : a / b < mediant a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Classical.choice, Quot.sounddfcd538c9ad0865d744d81d02ffd0e07028e02db0ca89401d7aa1cc66c8a0a35The mediant is strictly larger than the smaller of the two fractions.
LeanFrontier.Mediant.mediant_lt_div{a b c d : K} (hb : 0 < b) (hd : 0 < d) (h : a / b < c / d) : mediant a b c d < c / d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Classical.choice, Quot.sound2a79fa0e5c8520f3d2fa6b2fc5ee8ac23db94bc9053cb22024645311e40dc13bThe mediant is strictly smaller than the larger of the two fractions.
LeanFrontier.PowerSums.sum_odd_eq_sq(n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2
import LeanFrontier.NumberTheory.PowerSums2636907985e7cc99ab78b2f099b0ddfa006bd4bb · downstream import passpropext, Classical.choice, Quot.sound34476c59800c620441c08612dc96771afcd1fad3e181d430558072b16fa1eddcThe first `n` odd natural numbers sum to `n²`.
LeanFrontier.PowerSums.sum_cubes_eq_sum_sq(n : ℕ) : (∑ i ∈ Finset.range n, i) ^ 2 = ∑ i ∈ Finset.range n, i ^ 3
import LeanFrontier.NumberTheory.PowerSums2636907985e7cc99ab78b2f099b0ddfa006bd4bb · downstream import passpropext, Classical.choice, Quot.sounde90e64d3c4716c9b63f002157e3f77539368a0cce94a4e9bfa0bd7daa79175b1Nicomachus's theorem: the sum of the first `n` cubes equals the square of the sum of the first `n` natural numbers.
LeanFrontier.SternDiatomic.fusc_two_mul(n : ℕ) : fusc (2 * n) = fusc n
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Quot.soundc1f244e0834d3809d7e960fd9a730b47c3d459e1062ef2e910d00b4722c99f15Halving an even index leaves the value unchanged.
LeanFrontier.SternDiatomic.fusc_two_mul_add_one(n : ℕ) : fusc (2 * n + 1) = fusc n + fusc (n + 1)
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Quot.sounda44f0f6d20e948e023b4bc8480843bb93612a1f6a8d5882c8e5cb8342cc2db70An odd index splits into the two neighbouring values at half the index.
LeanFrontier.SternDiatomic.coprime_fusc_fusc_succ(n : ℕ) : Nat.Coprime (fusc n) (fusc (n + 1))
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Classical.choice, Quot.sounda959969f48c0e19a8ae259e56cfa7e2d3683f98ce2a17e4ff300870f909b3effConsecutive values of Stern's diatomic sequence are coprime, so the fraction `fusc n / fusc (n + 1)` is always in lowest terms.
LeanFrontier.SternDiatomic.fusc_pos{n : ℕ} (hn : n ≠ 0) : 0 < fusc n
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Classical.choice, Quot.sound1a38f1af66849b7b793296a9ff6c9ee8285c771949d9056ba259925898f3004fEvery value of Stern's diatomic sequence after the initial one is positive.
LeanFrontier.Nat.two_le_sylvesterNumber(n : ℕ) : 2 ≤ sylvesterNumber n
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Quot.sound6948b3ebe1e937cca79ec29770e4953ea8633369b93826428efaf20bdcf7867cEvery term is at least `2`; in particular no term is `0` or `1`.
LeanFrontier.Nat.sylvesterNumber_succ_eq_sq_sub_add_one(n : ℕ) : sylvesterNumber (n + 1) = sylvesterNumber n ^ 2 - sylvesterNumber n + 1
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Quot.soundcf37838bb578357f9607c7e765fc6cdbf44b92a8d32004b01a9c9bc3db611835The defining recurrence in its classical form.
LeanFrontier.Nat.sylvesterNumber_eq_prod_add_one(n : ℕ) : sylvesterNumber n = (∏ i ∈ Finset.range n, sylvesterNumber i) + 1
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Classical.choice, Quot.sound51032bbf0bb61849a926ad476ae3f82efafe4c38efa7aac8f0f0906b8ad5d3b6Each term is one more than the product of all the earlier ones.
LeanFrontier.Nat.coprime_sylvesterNumber_sylvesterNumber{m n : ℕ} (h : m ≠ n) : Nat.Coprime (sylvesterNumber m) (sylvesterNumber n)
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Classical.choice, Quot.sound204ad1c3614d13c4c9ebaa3fde114b0c7bb5276c157fd7f3db57c9db85e259edDistinct terms of Sylvester's sequence are coprime.
LeanFrontier.Nat.strictMono_sylvesterNumber: StrictMono sylvesterNumber
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Quot.sound9db6a46f259be074e5039c727b708e129a21c4578b9c18b24795b3964764e536Sylvester's sequence is strictly increasing.
LeanFrontier.Nat.sum_range_inv_sylvesterNumber(n : ℕ) : ∑ i ∈ Finset.range n, (1 : K) / sylvesterNumber i = 1 - 1 / ((sylvesterNumber n : K) - 1)
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Classical.choice, Quot.sound7e3e2c3f07fc325b36056364777ce1bf31e62aae77931328950986947aea6469The reciprocals of Sylvester's sequence telescope: the partial sums of `1 / S i` are `1 - 1 / (S n - 1)`, so the greedy unit fraction expansion of `1` never overshoots.
LeanFrontier.HermiteLindemann.exp_injOn_isAlgebraic(hermiteLindemann : ∀ {z : ℂ}, z ≠ 0 → IsAlgebraic ℤ z → Transcendental ℤ (Complex.exp z)) : Set.InjOn Complex.exp {z : ℂ | IsAlgebraic ℤ z}
import LeanFrontier.NumberTheory.Transcendental.HermiteLindemann67f6771a4abe7dd5610f4d4a32c5abccd652a24a · downstream import passpropext, Classical.choice, Quot.sound3420106adbec770426cf0b8492918c4bedcb2e71b56ed9fdde9f4a988a30a46fHermite--Lindemann implies that complex exponentiation is injective when restricted to algebraic numbers.
LeanFrontier.FiniteGroupCharacter.sum_monoidHom_eq_zero_of_ne_one(chi : G →* R) (hchi : chi ≠ 1) : ∑ g : G, chi g = 0
import LeanFrontier.RepresentationTheory.FiniteGroupCharacter9d12a280a0722da3e56aac50f1bf413081a651c6 · downstream import passpropext, Classical.choice, Quot.sounda07f2b1c2d5e16305608cf860e2714c3ce04920cf59ce92a4bdfc415d49a1addA nontrivial monoid homomorphism from a finite group into a ring without zero divisors has sum zero.
LeanFrontier.Int.isTopologicalBasis_arithProgression: @IsTopologicalBasis ℤ furstenbergTopology {S : Set ℤ | ∃ a b, b ≠ 0 ∧ S = arithProgression a b}
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.soundcd6fe9610173e1fde1db2a1e99140ba3a9d0b2314444484aa66991f033be7d38The arithmetic progressions with nonzero step are a basis of the Furstenberg topology.
LeanFrontier.Int.isOpen_arithProgression(a b : ℤ) (hb : b ≠ 0) : IsOpen[furstenbergTopology] (arithProgression a b)
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sounddf75e75c08639fa35d3742c0eec46abe896ff20ae635d06c40831dfff88bf0deArithmetic progressions with nonzero step are open.
LeanFrontier.Int.isClosed_arithProgression(a : ℤ) {b : ℤ} (hb : b ≠ 0) : IsClosed[furstenbergTopology] (arithProgression a b)
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.soundfa74aaa726bab690656f9228808873c127b6dc34a024ddbe26da4ad629645fe6Arithmetic progressions with nonzero step are closed: after reducing to a positive step via `abs_dvd`, the complement is the union of the progressions shifted by the nonzero residues. Together with `isOpen_arithProgression`, the basic sets of the Furstenberg topology are clopen.
LeanFrontier.Int.infinite_arithProgression(a : ℤ) {b : ℤ} (hb : b ≠ 0) : (arithProgression a b).Infinite
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sound300240412febcfb60f08ca96cad0504a80c523c4eeaa5d929b4544ae1254b3a6An arithmetic progression with nonzero step is infinite.
LeanFrontier.Int.infinite_of_isOpen{U : Set ℤ} (hU : IsOpen[furstenbergTopology] U) (hne : U.Nonempty) : U.Infinite
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.soundd10a7b29b25c414cf49efa33d04a676b83ed60274b8626a0dff0d0ed0234b247Every nonempty open set of the Furstenberg topology is infinite: it contains a whole arithmetic progression around each of its points.
LeanFrontier.Int.iUnion_prime_arithProgression: ⋃ p ∈ {p : ℕ | p.Prime}, arithProgression 0 (p : ℤ) = ({1, -1} : Set ℤ)ᶜ
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sound47f380ba47d198cb18e10c545f39eff5c6f2b9156ea805ffc0ccbf235b22f552Furstenberg's covering identity: the progressions `pℤ` over all primes cover exactly the integers other than `1` and `-1`.
LeanFrontier.Int.infinite_of_iUnion_eq_compl{S : Set ℕ} (h0 : 0 ∉ S) (hcov : ⋃ p ∈ S, arithProgression 0 (p : ℤ) = ({1, -1} : Set ℤ)ᶜ) : S.Infinite
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sound52d6d8ff6b3f3963b7a91b2d5138ff4fbc011f85205aa4dc379b1947607636aeThe engine of Furstenberg's proof: a set of nonzero naturals whose progressions cover all of `ℤ \ {1, -1}` cannot be finite, since a finite union of closed progressions is closed, and `{1, -1}` cannot be open, being finite and nonempty. Applied to the set of primes via `iUnion_prime_arithProgression`, this yields the infinitude of primes, which Mathlib already states as `Nat.infinite_setOf_prime`.