theorem nakayama_proper_ideal_stays_proper {B : Type u_1} [CommRing B] {A : Type u_2} [Field A] (f : B →+* A) (hf_inj : Function.Injective ⇑f) (hf_fin : f.Finite) (I : Ideal B) (hI : I ≠ ⊤) : I • ⊤ ≠ ⊤

Nakayama step: if A is a finite injective extension of B as a B-module via f and I is a proper ideal of B, then IA is a proper B-submodule of A.

theorem isField_of_injective_finite_of_isField {B : Type u_1} [CommRing B] {A : Type u_2} [Field A] (f : B →+* A) (hf_inj : Function.Injective ⇑f) (hf_fin : f.Finite) : IsField B

Field propagation: if a domain B injects into a field A via a finite ring map, then B itself is a field.

theorem mvPolynomial_fin_succ_not_isField (k : Type u_1) [Field k] (n : ℕ) : ¬IsField (MvPolynomial (Fin (n + 1)) k)

A polynomial ring k[x_1,...,x_{n+1}] with at least one variable is never a field.

theorem zariski_lemma_textbook_proof (k : Type u_1) (A : Type u_2) [Field k] [Field A] [Algebra k A] [Algebra.FiniteType k A] : Algebra.IsAlgebraic k A

Zariski's lemma, proved by chaining Noether normalization with the Nakayama field propagation: any finitely generated k-algebra that is a field is algebraic over k.