case H
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_3
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_4
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.360842
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.360872
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.361260
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.361651
ι'' : Type ?u.361654
M₂ : Type u_2
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.361687
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ↑(compLinearMap 0 g) x✝ = ↑0 x✝
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_3
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_4
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.360842
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.360872
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.361260
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.361651
ι'' : Type ?u.361654
M₂ : Type u_2
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.361687
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →ₗ[R] M
⊢ compLinearMap 0 g = 0
ext
no goals
case H
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_3
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_4
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.360842
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.360872
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.361260
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.361651
ι'' : Type ?u.361654
M₂ : Type u_2
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.361687
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ↑(compLinearMap 0 g) x✝ = ↑0 x✝
simp only [compLinearMap_apply, zero_apply]