case h
α : Type u_1
M : Type u_2
N : Type ?u.86392
P : Type ?u.86395
R : Type u_3
S : Type ?u.86401
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ ↑l a✝ = ↑0 a✝
α : Type u_1
M : Type u_2
N : Type ?u.86392
P : Type ?u.86395
R : Type u_3
S : Type ?u.86401
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
l : α →₀ M
h : l ∈ supported M R ∅
⊢ l = 0
ext
no goals
case h
α : Type u_1
M : Type u_2
N : Type ?u.86392
P : Type ?u.86395
R : Type u_3
S : Type ?u.86401
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ ↑l a✝ = ↑0 a✝
simp_all [mem_supported']