rw [leadingTerms_eq_self_iff_isHomogeneous]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).leadingTerms = X s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).IsHomogeneous (X s).totalDegree