Mv Hasse Deriv
Abstract
The multivariate Hasse derivative acts on monomials by binomial coefficients.
Definition 1.1 (Mv Hasse Deriv).
Lean statement: D5/S3/Arith/DiophantineApproximation/MvHasseDeriv.hasseDeriv
Formalization. D5/S3/Arith/DiophantineApproximation/MvHasseDeriv.hasseDeriv (✓ std3).
Citation. Ralf Stephan (2026). Subspace-Theorems. URL: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8.
Commentary.
The multivariate Hasse derivative acts on monomials by binomial coefficients.