Polynomial identities from evaluation at invertible matrices

We prove MvPolynomial.eq_of_eval_eq_on_gl: two polynomials in MvPolynomial (m × m) k over an infinite field k are equal if their evaluations agree at every invertible matrix. The proof uses that the set of invertible matrices is Zariski-dense in Matrix m m k.

theorem MvPolynomial.eq_of_eval_eq_on_gl {m : Type u_1} {k : Type u_2} [Fintype m] [DecidableEq m] [Field k] [Infinite k] {p q : MvPolynomial (m × m) k} (h : ∀ (g : GL m k), (eval fun (ij : m × m) => ↑g ij.1 ij.2) p = (eval fun (ij : m × m) => ↑g ij.1 ij.2) q) : p = q

Two polynomials in MvPolynomial (m × m) k over an infinite field k are equal if their evaluations agree at every invertible matrix.

The proof considers (p - q) * det(X), where det(X) := Matrix.det (Matrix.mvPolynomialX m m k) is the generic determinant polynomial. Evaluated at any s : m × m → k, this product vanishes: if det (Matrix.of fun i j => s (i, j)) = 0 the determinant factor kills it; otherwise the matrix is invertible and the hypothesis applies. By MvPolynomial.funext the product is zero, and since det(X) ≠ 0 and MvPolynomial _ k is an integral domain, p = q.