Theorem MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree

Modification history

2025-12-09 15:53
Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
feat(RingTheory): smooth algebras have smooth Noetherian models (#25143) …
Added MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degreeView on Github →