ArtinSchreierPrimeToDegree.lean

theorem exists_nat_shift_pos_not_dvd
    (p d : ℕ) (hd : 0 < d) (hpd : ¬ p ∣ d) (m : ℤ) :
    ∃ n : ℕ, 0 < m + (n : ℤ) * d ∧ ¬ (p : ℤ) ∣ m + (n : ℤ) * d

theorem normalized_mul_not_pow_sub
    {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete v] (π : K) (hπ : v π = WithZero.exp (-1 : ℤ))
    (p : ℕ) (hp : 1 < p) (hpd : ¬ p ∣ Module.finrank K L) (a : L) (ha : a ≠ 0) :
    ∃ b : K, ∀ y : L, y ^ p - y ≠ algebraMap K L b * a

theorem CompleteDVF.exists_mul_not_pow_sub_of_not_dvd_finrank
    {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (base : CompleteDVF K) (p : ℕ) (hp : 1 < p)
    (hpd : ¬ p ∣ Module.finrank K L) (a : L) (ha : a ≠ 0) :
    ∃ b : K, ∀ y : L, y ^ p - y ≠ algebraMap K L b * a

theorem CompleteDVF.exists_moved_pow_sub_class_of_not_dvd_finrank
    {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (base : CompleteDVF K) (p : ℕ) (hp : 1 < p)
    (hpd : ¬ p ∣ Module.finrank K L) (τ : L ≃ₐ[K] L) (hτ : τ ≠ 1) :
    ∃ x : L, ∀ y : L, y ^ p - y ≠ τ x - x