R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.71594
B' : Type ?u.71597
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ AddMonoidAlgebra.single 0 (↑(algebraMap R A) r) = ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.71594
B' : Type ?u.71597
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (↑C (↑(algebraMap R A) r)).toFinsupp = ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r
rw [toFinsupp_C]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.71594
B' : Type ?u.71597
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ AddMonoidAlgebra.single 0 (↑(algebraMap R A) r) = ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r
rfl