Polynomial method in char p without Hasse derivatives: Frobenius descent in Lean

If a minimal-degree argument needs a nonzero partial derivative (joints theorem, etc.), char p breaks it only when all pderiv i Q = 0. Then every exponent m_i of Q is 0 in K, so by ExpChar cases (rcases on the instance: zero case gives Q constant, prime case gives CharP) q | m_i, and Q = expand q R with deg R < deg Q. Build R as ∑ m' ∈ Q.support.image (mapRange (·/q)), monomial m' (Q.coeff (q • m')); prove Q = expand q R by ext m splitting on ∀ i, q ∣ m i with coeff_expand_smul / coeff_expand_of_not_dvd. Use q := ringExpChar K (instance ringExpChar.expChar). eval_expand reads eval f (expand p φ) = eval (f ^ p) φ with Pi power, so use x ^ q on vectors directly; linear independence survives via RingHom.map_det (frobenius K q) + Matrix.linearIndependent_row_iff_isUnit. Gotcha: MvPolynomial is no longer defeq-usable as a Finsupp (Finsupp.onFinset doesn't typecheck as MvPolynomial), and MvPolynomial.coeff_zero is deprecated for AddMonoidAlgebra.coeff_zero. Do the minimal-counterexample induction over all configurations, since the twist changes the point set.