Nilpotents and units in multivariate polynomial rings

We prove that

• MvPolynomial.isNilpotent_iff: A multivariate polynomial is nilpotent iff all its coefficients are.
• MvPolynomial.isUnit_iff: A multivariate polynomial is invertible iff its constant term is invertible and its other coefficients are nilpotent.

theorem MvPolynomial.isNilpotent_iff {σ : Type u_1} {R : Type u_2} [CommRing R] {P : MvPolynomial σ R} : IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (P.coeff i)

instance MvPolynomial.instIsReduced {σ : Type u_1} {R : Type u_2} [CommRing R] [IsReduced R] : IsReduced (MvPolynomial σ R)

theorem MvPolynomial.isUnit_iff {σ : Type u_1} {R : Type u_2} [CommRing R] {P : MvPolynomial σ R} : IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

instance MvPolynomial.instIsLocalHomRingHomC {σ : Type u_1} {R : Type u_2} [CommRing R] : IsLocalHom C

instance MvPolynomial.instIsLocalHomRingHomAlgebraMap {σ : Type u_1} {R : Type u_2} [CommRing R] : IsLocalHom (algebraMap R (MvPolynomial σ R))

theorem MvPolynomial.isUnit_iff_totalDegree_of_isReduced {σ : Type u_1} {R : Type u_2} [CommRing R] {P : MvPolynomial σ R} [IsReduced R] : IsUnit P ↔ IsUnit (P.coeff 0) ∧ P.totalDegree = 0

theorem MvPolynomial.isUnit_iff_eq_C_of_isReduced {σ : Type u_1} {R : Type u_2} [CommRing R] {P : MvPolynomial σ R} [IsReduced R] : IsUnit P ↔ ∃ (r : R), IsUnit r ∧ P = C r