structure TopologicalGroupProp (G : Type u_1) [TopologicalSpace G] [Group G] : Prop

Proposition-valued version of IsTopologicalGroup: a group $G$ with a topology such that multiplication and inversion are continuous. Used as a Prop (rather than a structure) so it can be carried through hypotheses without instance issues.

• mul_continuous : Continuous fun (p : G × G) => p.1 * p.2
• inv_continuous : Continuous Inv.inv

theorem TopologicalGroupProp.of_isTopologicalGroup (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : TopologicalGroupProp G

From a Mathlib IsTopologicalGroup instance, derive TopologicalGroupProp.

theorem TopologicalGroupProp.toIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] (h : TopologicalGroupProp G) : IsTopologicalGroup G

From TopologicalGroupProp, construct an IsTopologicalGroup instance.

theorem valuationRing_isOpen (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsOpen ↑Valued.v.valuationSubring

Valuation subring is open: in a valued field $K$, the valuation subring $\mathcal{O}_v = \{x \in K : v(x) \le 1\}$ is an open subset of $K$.

theorem valuationRing_isClosed (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClosed ↑Valued.v.valuationSubring

Valuation subring is closed: the valuation subring is also closed in $K$ — this is the non-archimedean analogue of the fact that closed balls are closed.

theorem valuationRing_isClopen (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClopen ↑Valued.v.valuationSubring

Valuation subring is clopen: combining the two preceding results, $\mathcal{O}_v$ is both open and closed in $K$ (i.e. clopen).

theorem maximalIdeal_isOpen (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsOpen {x : K | Valued.v.restrict x < 1}

Maximal ideal of the valuation subring is open in $K$: the set $\{x : v(x) < 1\}$ — which corresponds to the maximal ideal $\mathfrak{m}_v$ of $\mathcal{O}_v$ — is open.

theorem maximalIdeal_isClosed (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClosed {x : K | Valued.v.restrict x < 1}

Maximal ideal of the valuation subring is closed in $K$: $\{x : v(x) < 1\}$ is closed (another non-archimedean phenomenon — strict inequality balls are closed).

theorem maximalIdeal_isClopen (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClopen {x : K | Valued.v.restrict x < 1}

Maximal ideal is clopen in $K$: combining the two preceding results.

theorem valuationUnits_isOpen (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsOpen {x : K | Valued.v.restrict x = 1}

The set of valuation units is open in $K$: $\mathcal{O}_v^\times = \{x : v(x) = 1\}$ is open.

theorem valuationUnits_isClosed (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClosed {x : K | Valued.v.restrict x = 1}

The set of valuation units is closed in $K$: $\{x : v(x) = 1\}$ is also closed.

theorem valuationUnits_isClopen (K : Type u) [Field K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClopen {x : K | Valued.v.restrict x = 1}

Valuation units form a clopen subset of $K$: combining the two preceding results.

noncomputable def newtonStep {R : Type u_1} [CommRing R] (f : Polynomial R) (x : R) (h_unit : IsUnit (Polynomial.eval x (Polynomial.derivative f))) : R

One Newton iteration: given $f \in R[X]$ and a current approximation $x$ at which $f'(x)$ is a unit, return $x - f(x)/f'(x)$. The unit hypothesis lets us invert $f'(x)$.

noncomputable def newtonSeq {R : Type u_1} [CommRing R] (f : Polynomial R) (x₀ : R) : ℕ → R

Newton iteration sequence starting from $x_0$: $c_0 = x_0$ and $c_{n+1} = c_n - f(c_n) \cdot \text{Ring.inverse}(f'(c_n))$. We use Ring.inverse so that this is total in $R$ — the value is meaningful when $f'(c_n)$ is a unit.

theorem hensel_nonmonic_adic (R : Type u_1) [CommRing R] (I : Ideal R) [IsAdicComplete I R] (f : Polynomial R) (a₀ : R) (h₁ : Polynomial.eval a₀ f ∈ I) (h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f)))) : ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I

Hensel's lemma for non-monic polynomials over an adically complete ring: if $R$ is $I$-adically complete, $f \in R[X]$ has an approximate root $a_0$ with $f(a_0) \in I$ and $f'(a_0)$ a unit mod $I$, then there is a true root $a \in R$ of $f$ with $a \equiv a_0 \pmod I$. The proof constructs Newton's sequence $c_{n+1} = c_n - f(c_n)/f'(c_n)$, shows it is Cauchy in the $I$-adic topology, and takes its limit.

theorem hensel_nonmonic_adic_newton (R : Type u_1) [CommRing R] (I : Ideal R) [IsAdicComplete I R] (f : Polynomial R) (a₀ : R) (h₁ : Polynomial.eval a₀ f ∈ I) (h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f)))) : ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I ∧ (∀ (n : ℕ), newtonSeq f a₀ n ≡ a [SMOD I ^ n • ⊤]) ∧ (∀ (n : ℕ), Polynomial.eval (newtonSeq f a₀ n) f ∈ I ^ (n + 1)) ∧ ∀ (n : ℕ), IsUnit (Polynomial.eval (newtonSeq f a₀ n) (Polynomial.derivative f))

Hensel's lemma with an explicit Newton-sequence witness: same hypotheses as hensel_nonmonic_adic, but the conclusion also records that the Newton sequence converges to $a$ in the $I$-adic topology, that $f(\text{newtonSeq}\,f\,a_0\,n) \in I^{n+1}$ for every $n$ (quadratic convergence!), and that $f'(\text{newtonSeq}\,f\,a_0\,n)$ is a unit at every step (allowing the iteration to continue). This stronger form is what IwahoriDecomp consumes.