theorem Ideal.generators_iff_cotangent_span (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (s : Set ↥(IsLocalRing.maximalIdeal R)) : span (Subtype.val '' s) = IsLocalRing.maximalIdeal R ↔ Submodule.span (IsLocalRing.ResidueField R) (⇑(IsLocalRing.maximalIdeal R).toCotangent '' s) = ⊤

Corollary 18.4 (Nakayama, set form): for a local Noetherian ring $R$ with maximal ideal $\mathfrak{m}$ and a subset $s \subseteq \mathfrak{m}$, the elements of $s$ generate $\mathfrak{m}$ as an ideal iff their images in the cotangent space $\mathfrak{m}/\mathfrak{m}^2$ span it as an $R/\mathfrak{m}$-vector space.

theorem Ideal.generators_iff_cotangent_span_fin (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {n : ℕ} (t : Fin n → ↥(IsLocalRing.maximalIdeal R)) : span (Set.range fun (i : Fin n) => ↑(t i)) = IsLocalRing.maximalIdeal R ↔ Submodule.span (IsLocalRing.ResidueField R) (Set.range fun (i : Fin n) => (IsLocalRing.maximalIdeal R).toCotangent (t i)) = ⊤

Finite-tuple version of Corollary 18.4: for $t_1, \dots, t_n \in \mathfrak{m}$ in a local Noetherian ring, the $t_i$ generate $\mathfrak{m}$ iff their images generate $\mathfrak{m}/\mathfrak{m}^2$ as an $R/\mathfrak{m}$-vector space.