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

State before:
R✝ : Type ?u.286962
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
⊢ homogenization i (X j ^ n - 1) = X j ^ n - X i ^ n
Tactic:
convert homogenization_X_pow_sub_C hn (R := R) _
State after:
case h.e'_3.h.e'_6
R✝ : Type ?u.286962
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
⊢ X i ^ n = C 1 * X i ^ n

State before:
case h.e'_3.h.e'_6
R✝ : Type ?u.286962
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
⊢ X i ^ n = C 1 * X i ^ n
Tactic:
simp
State after:
no goals