k : Type u₁
G : Type u₂
R : Type ?u.2755514
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2755551
inst✝¹ : Semiring B
inst✝ : Algebra k B
φ₁ : AddMonoidAlgebra k G →ₐ[k] A
x✝ : G
⊢ ↑φ₁ (Finsupp.single x✝ 1) = ↑φ₁ (Finsupp.single x✝ 1)
k : Type u₁
G : Type u₂
R : Type ?u.2755514
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2755551
inst✝¹ : Semiring B
inst✝ : Algebra k B
φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A
⊢ φ₁ = φ₂ → ∀ (x : G), ↑φ₁ (Finsupp.single x 1) = ↑φ₂ (Finsupp.single x 1)
rintro rfl _
no goals
k : Type u₁
G : Type u₂
R : Type ?u.2755514
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2755551
inst✝¹ : Semiring B
inst✝ : Algebra k B
φ₁ : AddMonoidAlgebra k G →ₐ[k] A
x✝ : G
⊢ ↑φ₁ (Finsupp.single x✝ 1) = ↑φ₁ (Finsupp.single x✝ 1)
rfl