R : Type u_1
inst✝ : Semiring R
this : X = ↑(monomial 1) 1
⊢ ↑toLaurent X = T 1
R : Type u_1
inst✝ : Semiring R
⊢ ↑toLaurent X = T 1
have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]
no goals
R : Type u_1
inst✝ : Semiring R
this : X = ↑(monomial 1) 1
⊢ ↑toLaurent X = T 1
simp [this, Polynomial.toLaurent_C_mul_T]
no goals
R : Type u_1
inst✝ : Semiring R
⊢ X = ↑(monomial 1) 1
simp [← C_mul_X_pow_eq_monomial]