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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ homogenization i (homogenization i p) = homogenization i p
Tactic:
classical
apply homogenization_of_isHomogeneous p.totalDegree
exact isHomogeneous_homogenization _ _
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ homogenization i (homogenization i p) = homogenization i p
Tactic:
apply homogenization_of_isHomogeneous p.totalDegree
State after:
case hp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree

State before:
case hp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Tactic:
exact isHomogeneous_homogenization _ _
State after:
no goals