CompletedPrimitiveIrreducible.lean

theorem padicCompletedUnramifiedIntegerMap_isUniformizer
    (p : ℕ) [Fact p.Prime] :
    let π :=
      padicIntEquivValuationSubring p (p : ℤ_[p])
    (padicCompletedUnramifiedCompleteDVF p).valuation.IsUniformizer
      ((padicCompletedUnramifiedIntegerMap p π :
        (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
          padicCompletedUnramifiedField p) := by
  let F := padicLocalField p
  let base := F.toCompleteDVF
  let target := padicCompletedUnramifiedCompleteDVF p
  let π : (padicLocalField p).valuationSubring :=
    padicIntEquivValuationSubring p (p : ℤ_[p])
  let πE : target.valuationSubring :=
    padicCompletedUnramifiedIntegerMap p π
  have hπ : base.valuation.IsUniformizer (π : ℚ_[p]) := by
    simpa only [F, base, π] using
      padicMultiplicativeLubinTateSeries_isUniformizer p
  obtain ⟨ϖ, hϖ⟩ := target.exists_uniformizer
  apply hϖ.of_associated
  rw [← Ideal.span_singleton_eq_span_singleton]
  calc
    Ideal.span ({ϖ} : Set target.valuationSubring) =
        target.maximalIdeal :=
      (target.maximalIdeal_eq_span_uniformizer hϖ).symm
    _ =
        Ideal.map (padicCompletedUnramifiedIntegerMap p)
          base.maximalIdeal := by
      simpa only [F, base, target] using
        (padicCompletedUnramifiedIntegerMap_map_maximalIdeal p).symm
    _ =
        Ideal.map (padicCompletedUnramifiedIntegerMap p)
          (Ideal.span
            ({π} : Set (padicLocalField p).valuationSubring)) := by
      exact congrArg (Ideal.map (padicCompletedUnramifiedIntegerMap p))
        (base.maximalIdeal_eq_span_uniformizer hπ)
    _ = Ideal.span ({πE} : Set target.valuationSubring) := by
      rw [Ideal.map_span, Set.image_singleton]

theorem padicCompletedPrimitivePolynomialInteger_natDegree
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomialInteger p n).natDegree =
      (p - 1) * p ^ n

theorem padicCompletedPrimitivePolynomialInteger_isEisensteinAt
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomialInteger p n).IsEisensteinAt
      (padicCompletedUnramifiedCompleteDVF p).maximalIdeal

theorem padicCompletedPrimitivePolynomialInteger_irreducible
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Irreducible (padicCompletedPrimitivePolynomialInteger p n)

theorem padicCompletedPrimitivePolynomial_irreducible
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Irreducible (padicCompletedPrimitivePolynomial p n)