α : Type u_1
M : Type u_2
N : Type ?u.32590
P : Type ?u.32593
R : Type u_3
S : Type ?u.32599
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
⊢ ∀ ⦃x : α →₀ M⦄, (∀ (i : α), ↑x i = 0) → x = 0
α : Type u_1
M : Type u_2
N : Type ?u.32590
P : Type ?u.32593
R : Type u_3
S : Type ?u.32599
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
⊢ (⨅ (a : α), ker (lapply a)) ≤ ⊥
simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]
no goals
α : Type u_1
M : Type u_2
N : Type ?u.32590
P : Type ?u.32593
R : Type u_3
S : Type ?u.32599
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
⊢ ∀ ⦃x : α →₀ M⦄, (∀ (i : α), ↑x i = 0) → x = 0
exact fun a h => Finsupp.ext h