rw [l]
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
l : coords (mulMonom 0 h tail) x₀ = 0 := mul_monom_zero h x₀ tail
⊢ coords (mulMonom 0 h tail) x₀ = 0
no goals