Theorem: MvPolynomial.leadingTerms_idempotent (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.leadingTerms = p.leadingTerms
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous, totalDegree_leadingTerms]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.IsHomogeneous p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.IsHomogeneous p.totalDegree
Tactic:
exact isHomogeneous_leadingTerms p
State after:
no goals