LeanPool.Monsky.Appendix

Imported Lean Pool material for LeanPool.Monsky.Appendix.

theorem LeanPool.Monsky.mul_del_commute {R : Type} [CommRing R] (p : Polynomial R) (n : ℕ) : Polynomial.C 2 * Polynomial.erase n p = Polynomial.erase n (Polynomial.C 2 * p)

theorem LeanPool.Monsky.erase_degree_leq_n (R : Type) [CommRing R] (p : Polynomial R) (n : ℕ) (h1 : n > 0) (h2 : p.natDegree ≤ n) : (Polynomial.erase n p).natDegree < n

theorem LeanPool.Monsky.pow_mul_inv_pow_of_le {α : ℝ} (hα : α ≠ 0) {n x : ℕ} (h : x ≤ n) : α ^ n * (α ^ x)⁻¹ = α ^ (n - x)

For nonzero α and x ≤ n, we have α ^ n * (α ^ x)⁻¹ = α ^ (n - x).

theorem LeanPool.Monsky.erase_natDegree_lt_or_zero {B : Subring ℝ} {q1 : Polynomial ↥B} {n : ℕ} (deg1 : q1.natDegree ≤ n) : (Polynomial.erase n q1).natDegree < n ∨ (Polynomial.erase n q1).natDegree = 0

The degree of q1.erase n is either < n or 0, given q1.natDegree ≤ n.

theorem LeanPool.Monsky.lower_degree (B : Subring ℝ) (α : ℝ) (m n : ℕ) (H : α ∉ B ∧ α⁻¹ ∉ B) (p q : Polynomial ↥B) (m_eq_degree_p : p.natDegree = m) (n_eq_degree_q : q.natDegree = n) (zero_lt_m : m ≠ 0) (zero_lt_n : n ≠ 0) (p_eval : (Polynomial.aeval α) p = 1 / 2) (q_eval : (Polynomial.aeval α⁻¹) q = 1 / 2) (leq : n ≤ m) : ∃ (m' : ℕ) (pq : Polynomial ↥B), m' < m ∧ (Polynomial.aeval α) pq = 1 / 2 ∧ m' = pq.natDegree

theorem LeanPool.Monsky.inclusion_maximal_valuation (B : Subring ℝ) (h1 : 1 / 2 ∉ B) (h2 : ∀ (C : Subring ℝ), B ≤ C ∧ 1 / 2 ∉ C → B = C) : ∃ (D : ValuationSubring ℝ), D.toSubring = B

def LeanPool.Monsky.S : Set (Subring ℝ)

The set of subrings of ℝ not containing 1/2.

Equations

• LeanPool.Monsky.S = {A : Subring ℝ | 1 / 2 ∉ A}

def LeanPool.Monsky.Z : Subring ℝ

The image of ℤ inside ℝ as a subring.

Equations

• LeanPool.Monsky.Z = (Int.castRingHom ℝ).range

theorem LeanPool.Monsky.Z_in_S : Z ∈ S

theorem LeanPool.Monsky.sUnion_is_ub (c : Set (Subring ℝ)) : c ⊆ S → IsChain (fun (x1 x2 : Subring ℝ) => x1 ≤ x2) c → ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

theorem LeanPool.Monsky.valuation_ring_no_half : ∃ (B : ValuationSubring ℝ), 1 / 2 ∉ B

theorem LeanPool.Monsky.non_archimedean (Γ₀ : Type) [LinearOrderedCommGroupWithZero Γ₀] (K : Type) [Field K] (v : Valuation K Γ₀) (x y : K) : v x ≠ v y → v (x + y) = max (v x) (v y)

theorem LeanPool.Monsky.valuation_on_reals : ∃ (Γ₀ : Type) (x : LinearOrderedCommGroupWithZero Γ₀) (v : Valuation ℝ Γ₀), v (1 / 2) > 1

theorem LeanPool.Monsky.odd_valuation (Γ₀ : Type) (x✝ : LinearOrderedCommGroupWithZero Γ₀) (v : Valuation ℝ Γ₀) (vhalf : v (1 / 2) > 1) (n : ℕ) : Odd n → v (1 / ↑n) = 1