Minkowski's theorem to Zeckendorf's theorem

TheoremNiven's theorem#

Niven's theorem: The only rational values of cos that occur at rational multiples of π are {-1, -1/2, 0, 1/2, 1}.

niven {θ : ℝ} (hθ : ∃ r, θ = ↑r * Real.pi) (hcos : ∃ q, Real.cos θ = ↑q) :
  Real.cos θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}
Sources
Mathlibniven
Uses 9
Statement usesCos (extension of trigonometric functions to the complex plane)
Proof usesBasis · Characteristic p · Completeness · Field \(\C\) of complex numbers · Integral root theorem · Normed vector space over a normed field · Ordered ring · The Fundamental Theorem of Arithmetic

TheoremOstrowski's theorem#

Mathlib records this with 2 declarations.

Rat.AbsoluteValue.equiv_real_or_padic: Ostrowski's Theorem: every absolute value (with values in ℝ) on ℚ is equivalent to either the standard absolute value or a p-adic absolute value for a prime p.

Rat.AbsoluteValue.equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) :
  f ≈ Rat.AbsoluteValue.real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ Rat.AbsoluteValue.padic p

RatFunc.valuation_isEquiv_infty_or_adic: Ostrowski's Theorem for K(X) with K any field: A valuation trivial on K is equivalent either to the valuation at infinity or to the p-adic valuation for a unique maximal ideal p of K[X].

RatFunc.valuation_isEquiv_infty_or_adic.{u_1, u_2} {K : Type u_1} {Γ : Type u_2} [Field K]
  [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [Valuation.IsTrivialOn K v]
  [v.IsNontrivial] [DecidableEq (RatFunc K)] :
  Xor (v.IsEquiv (RatFunc.inftyValuation K))
    (∃! u, v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u))
Sources
MathlibRat.AbsoluteValue.equiv_real_or_padic · RatFunc.valuation_isEquiv_infty_or_adic
Uses 24
Statement uses\(K[X]\) is Euclidean · Associative algebra over a commutative ring · Field \(\R\) of real numbers · Field of fractions of an integral domain · Greatest common divisor · Least common multiple · Linear map · Maximal ideal · Noetherian module · Order · Prime ideal · Rational fraction fields with one indeterminate over a field · The Fundamental Theorem of Arithmetic
Proof usesArray · Characteristic p · Coprime element · Field \(\Q\) of rational numbers · Local ring · Logarithm · Metric space · Order topology · Ordered ring · Sum of subspaces · Topological ring

TheoremPentagonal number theorem#

Mathlib records this with 2 declarations.

PowerSeries.WithPiTopology.hasProd_one_sub_X_pow: Pentagonal number theorem for power series, expressed as an infinite product. See also PowerSeries.WithPiTopology.hasSum_pentagonalSeries that expresses pentagonalSeries as an infinite sum.

PowerSeries.WithPiTopology.hasProd_one_sub_X_pow.{u_1} (R : Type u_1) [CommRing R]
  [TopologicalSpace R] :
  HasProd (fun n => 1 - PowerSeries.X ^ (n + 1)) (PowerSeries.pentagonalSeries R)

hasProd_eulerFunction: Pentagonal number theorem for Euler function, expressed as an infinite product. See hasSum_eulerFunction_pentagonal that expresses eulerFunction as an infinite sum.

hasProd_eulerFunction.{u_1} {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  {x : R} (hx : ‖x‖ < 1) : HasProd (fun n => 1 - x ^ (n + 1)) (eulerFunction x)
Sources
MathlibPowerSeries.WithPiTopology.hasProd_one_sub_X_pow · hasProd_eulerFunction
Uses 12
Statement usesCompleteness · Infinite sum · Linear map · Metric space · Power series · Ring structure \(\Z\)
Proof usesAbsolutely convergent series in Banach spaces · Characteristic zero · Closure · Hausdorff space · Order topology · Topological ring

TheoremVon Staudt–Clausen theorem#

von Staudt-Clausen theorem: For any natural number \(k\), the sum $\(B_{2k} + \sum_{p - 1 \mid 2k} \frac{1}{p}\)$ is an integer.

Bernoulli.vonStaudt_clausen (k : ℕ) :
  bernoulli (2 * k) + ∑ p ∈ Finset.range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p ∈
    Set.range Int.cast
Sources
MathlibBernoulli.vonStaudt_clausen
Uses 5
Statement usesBernoulli numbers · Irreducible element
Proof usesRing structure \(\Z\) · Subring · Sum of kth powers

DefinitionZeckendorf's theorem#

Zeckendorf's Theorem as an equivalence between natural numbers and Zeckendorf representations. Every natural number can be written uniquely as a sum of non-consecutive Fibonacci numbers (if we forget about the first two terms F₀ = 0, F₁ = 1).

Nat.zeckendorfEquiv : ℕ ≃ { l // l.IsZeckendorfRep }
Sources
MathlibNat.zeckendorfEquiv
Uses 2
Statement usesList · Natural number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.