Theorem: MvPolynomial.homogeneousSubmodule_eq_finsupp_supported (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_1
τ : Type ?u.9961
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.9970
n : ℕ
⊢ homogeneousSubmodule σ R n = Finsupp.supported R R {d | degree d = n}
Tactic:
convert weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n
State after:
no goals