Complex points of finite-type algebras

Every nonzero commutative ℂ-algebra of finite type admits a ℂ-point: quotient by a maximal ideal, apply Zariski's lemma over the Jacobson ring ℂ, and lift to the algebraically closed base. This is the Nullstellensatz input of the descent's final step.

theorem RS.exists_algHom_complex (R : Type u_1) [CommRing R] [Algebra ℂ R] [Nontrivial R] [Algebra.FiniteType ℂ R] : Nonempty (R →ₐ[ℂ] ℂ)

The ℂ-point: a nonzero finite-type commutative ℂ-algebra maps onto ℂ.