theorem dim_affine_space (k : Type) [Field k] (n : ℕ) : Algebra.trdeg k (MvPolynomial (Fin n) k) = ↑n

Affine $n$-space $\mathbb{A}^n_k$ has dimension $n$: the transcendence degree of $k[x_1, \dots, x_n]$ over $k$ is $n$.

theorem quotient_eval_ker_isAlgebraic (k : Type) [Field k] {n : ℕ} (p : Fin n → k) : Algebra.IsAlgebraic k (MvPolynomial (Fin n) k ⧸ RingHom.ker (MvPolynomial.eval p))

The coordinate ring of a point $p \in \mathbb{A}^n_k$, i.e. $k[x_1, \dots, x_n] / \ker(\mathrm{eval}_p)$, is an algebraic extension of $k$ (in fact isomorphic to $k$).