Other results
Results named in the rest of Tau Ceti's TauCeti.NumberTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremCho's exponent identity#
The two deformation exponents differ by the density exponent:
N_Q = N_M + N.
TauCeti.DyadicJordanProfile.nQ_eq_nM_add_densityExponent (P : TauCeti.DyadicJordanProfile) :
P.nQ = P.nM + P.densityExponent
Lean
Formalized in Tau Ceti as TauCeti.DyadicJordanProfile.nQ_eq_nM_add_densityExponent.
Sources
TheoremDedekind's criterion for a quadratic order#
Let r be a root of X² - b X - a modulo
p, so that b - r is the second root. Then p factors as (p) = (p, ω - r) (p, ω - (b - r))
in ℤ[ω] if and only if p does not divide both the derivative 2r - b and the quotient
(r² - b r - a)/p, that is, unless p ∣ 2r - b and p² ∣ r² - b r - a.
QuadraticAlgebra.span_natCast_omega_sub_mul_span_natCast_omega_sub_eq_iff {a b : ℤ} {p : ℕ} {r : ℤ}
[Fact (Nat.Prime p)] (hr : ↑p ∣ r ^ 2 - b * r - a) :
Ideal.span {↑p, QuadraticAlgebra.omega - ↑r} *
Ideal.span {↑p, QuadraticAlgebra.omega - ↑(b - r)} =
Ideal.span {↑p} ↔
¬(↑p ∣ 2 * r - b ∧ ↑p ^ 2 ∣ r ^ 2 - b * r - a)
Lean
Formalized in Tau Ceti as QuadraticAlgebra.span_natCast_omega_sub_mul_span_natCast_omega_sub_eq_iff.
Sources
TheoremDistinct-slopes splitting theorem#
Over a complete ultrametric normed field, any polynomial whose finite Newton slopes have multiplicity one splits into linear factors over the base field.
Polynomial.splits_of_nodup_newtonSlopes.{u_1} {K : Type u_1} [NormedField K] [IsUltrametricDist K]
[CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b)
(hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K}
(hf : (f.newtonSlopes v).Nodup) : f.Splits
TheoremThe exponent in Siegel's lemma is optimal#
For an m × (m + 1) integer system, Siegel's
lemma Int.Matrix.exists_ne_zero_int_vec_norm_le gives a nonzero integer solution of sup norm at
most ((m + 1) · max 1 ‖A‖) ^ m. For 0 < m no exponent e < m works, with any constant C:
the system b xᵢ = xᵢ₊₁ with b large has no nonzero integer solution of sup norm at most
C · max 1 ‖A‖ ^ e.
TauCeti.Int.Matrix.not_forall_exists_ne_zero_int_vec_norm_le {m : ℕ} (hm : 0 < m) {e : ℝ}
(he : e < ↑m) (C : ℝ) :
¬∀ (A : Matrix (Fin m) (Fin (m + 1)) ℤ), ∃ x, x ≠ 0 ∧ A.mulVec x = 0 ∧ ‖x‖ ≤ C * max 1 ‖A‖ ^ e
Lean
Formalized in Tau Ceti as TauCeti.Int.Matrix.not_forall_exists_ne_zero_int_vec_norm_le.
Sources
TheoremMarkoff's theorem#
Every positive Markoff triple x is obtained from (1, 1, 1) by a
finite word in the Vieta moves: x = R_{i₁} (R_{i₂} ⋯ (R_{i_k} (1, 1, 1))). No coordinate
permutation is needed.
TauCeti.exists_foldr_markoffVieta_eq {x : Fin 3 → ℤ} (hx : x ∈ TauCeti.positiveMarkoffTriples) :
∃ l, List.foldr TauCeti.markoffVieta 1 l = x
Lean
Formalized in Tau Ceti as TauCeti.exists_foldr_markoffVieta_eq.
Other forms
Markoff's theorem, as a characterisation. Formalized in Tau Ceti as TauCeti.mem_positiveMarkoffTriples_iff_exists_foldr.
TauCeti.mem_positiveMarkoffTriples_iff_exists_foldr {x : Fin 3 → ℤ} :
x ∈ TauCeti.positiveMarkoffTriples ↔ ∃ l, List.foldr TauCeti.markoffVieta 1 l = x
Sources
TheoremMinkowski's linear forms theorem#
Let A be an invertible real square matrix indexed by
a nonempty finite type ι, and let a i ≥ 0 be bounds whose product is at least |det A|. Then
some nonzero integer vector z satisfies |∑ j, A i j * z j| ≤ a i for every i.
Matrix.exists_ne_zero_int_abs_sum_mul_le.{u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
[Nonempty ι] (A : Matrix ι ι ℝ) (hA : A.det ≠ 0) {a : ι → ℝ} (ha : 0 ≤ a)
(h : |A.det| ≤ ∏ i, a i) : ∃ z, z ≠ 0 ∧ ∀ (i : ι), |∑ j, A i j * ↑(z j)| ≤ a i
Uses 1
TheoremNewton polygon irreducibility criterion#
If the valuation takes integer values on
nonzero elements, a polynomial f with nonzero constant coefficient whose finite slopes all
equal a rational number q, and whose degree is the denominator of q, is irreducible.
Polynomial.irreducible_of_forall_mem_newtonSlopes_eq.{u_1} {K : Type u_1} [Field K]
{v : AddValuation K (WithTop ℝ)} (hint : ∀ (x : K), x ≠ 0 → ∃ n, v x = ↑↑n) {f : Polynomial K}
(hf : f.coeff 0 ≠ 0) {q : ℚ} (hq : ∀ m ∈ f.newtonSlopes v, m = ↑q) (hden : q.den = f.natDegree) :
Irreducible f
Lean
Formalized in Tau Ceti as Polynomial.irreducible_of_forall_mem_newtonSlopes_eq.
Other forms
Newton polygon irreducibility criterion, coprime form. Formalized in Tau Ceti as Polynomial.irreducible_of_forall_mem_newtonSlopes_eq_div.
Polynomial.irreducible_of_forall_mem_newtonSlopes_eq_div.{u_1} {K : Type u_1} [Field K]
{v : AddValuation K (WithTop ℝ)} (hint : ∀ (x : K), x ≠ 0 → ∃ n, v x = ↑↑n) {f : Polynomial K}
(hf : f.coeff 0 ≠ 0) (hdeg : 0 < f.natDegree) {a : ℤ} (hcop : a.natAbs.Coprime f.natDegree)
(ha : ∀ m ∈ f.newtonSlopes v, m = ↑a / ↑f.natDegree) : Irreducible f
Sources
TheoremSylvester's law of inertia at a real place#
Two regular quadratic forms become isometric at a real place exactly when their signatures there agree.
QuadraticForm.equivalent_atRealPlace_iff_realSignature_eq.{u, v, v'} {K : Type u} [Field K]
{V : Type v} [AddCommGroup V] [_root_.Module K V] {W : Type v'} [AddCommGroup W]
[_root_.Module K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} [FiniteDimensional K V]
[FiniteDimensional K W] (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate)
(w : { w // w.IsReal }) :
QuadraticMap.Equivalent (Q.atRealPlace w) (R.atRealPlace w) ↔
Q.realSignature w = R.realSignature w
Lean
Formalized in Tau Ceti as QuadraticForm.equivalent_atRealPlace_iff_realSignature_eq.
Sources
Uses 1 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.