Rückert's basis theorem: Conv K m is Noetherian

Rückert's basis theorem [GR65, Chapter II, §B], by induction on m. Conv K 0 ≅ K is a field (every nonzero element is a unit). For m + 1: let I be a nonzero ideal, f ∈ I nonzero; a linear change L (exists_substEquiv_isRegularIn, Subst.lean) makes g = f ∘ L x_0-regular of order d, and it suffices to show that J = I ∘ L is finitely generated (finite generation transports along the automorphism). The Weierstrass division by g writes every element as q g + r with r of x_0-degree < d, and r = ∑_{j<d} convTail (slice_j) x_0^j, so Conv K (m+1) ⧸ (g) is a Conv K m-module generated by the classes of 1, x_0, …, x_0^{d-1}; over the Noetherian Conv K m (induction hypothesis) it is a Noetherian module, hence Noetherian as a Conv K (m+1)-module (isNoetherian_of_tower). The image of J in the quotient is therefore finitely generated, and so is J ∩ (g) = (g); hence J is finitely generated (Submodule.fg_of_fg_map_of_fg_inf_ker).

The Conv K m-module structures are local instances (a global Algebra (Conv K m) (Conv K (m+1)) instance makes instance search run very long). Noetherianity is what gives every ideal of germs a finite generating system (ZeroSet.lean) and the stalks of the structure sheaf of an analytic manifold their Noetherian structure (Hironaka/Manifold/Germ/StalkNoetherian.lean).

The coefficient field K is ℝ or ℂ ([RCLike K]).

theorem Analytic.isUnit_of_ne_zero_conv_zero {K : Type u_1} [RCLike K] {f : ↥(Conv K 0)} (hf : f ≠ 0) : IsUnit f

Every nonzero element of Conv K 0 is a unit.

theorem Analytic.isNoetherianRing_conv_zero {K : Type u_1} [RCLike K] : IsNoetherianRing ↥(Conv K 0)

Conv K 0 is Noetherian.

theorem Analytic.isNoetherianRing_conv_succ {K : Type u_1} [RCLike K] {m : ℕ} [IsNoetherianRing ↥(Conv K m)] : IsNoetherianRing ↥(Conv K (m + 1))

The inductive step: if Conv K m is Noetherian, so is Conv K (m+1) (Weierstrass division by a regular element makes the quotient a finite Conv K m-module) [GR65, Chapter II, §B].

theorem Analytic.isNoetherianRing_conv (K : Type u_1) [RCLike K] {m : ℕ} : IsNoetherianRing ↥(Conv K m)

Rückert's basis theorem: Conv K m is Noetherian [GR65, Chapter II, §B], by induction on m.

instance Analytic.instIsNoetherianRingConv (K : Type u_1) [RCLike K] {m : ℕ} : IsNoetherianRing ↥(Conv K m)

Rückert's basis theorem as an instance (the theorem isNoetherianRing_conv registered for instance search).