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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ homogenization i 1 = 1
Tactic:
simp only [homogenization, totalDegree_one, zero_tsub, add_zero, Finsupp.single_zero]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.mapDomain (fun j => j) 1 = 1

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.mapDomain (fun j => j) 1 = 1
Tactic:
erw [Finsupp.mapDomain_single]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.single 0 1 = 1

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.single 0 1 = 1
Tactic:
rfl
State after:
no goals