case H
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.362901
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.362931
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.363319
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
ι' : Type ?u.363710
ι'' : Type ?u.363713
M₂ : Type u_5
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.363746
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f₁ f₂ : AlternatingMap R M N ι
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ↑(compLinearMap (f₁ + f₂) g) x✝ = ↑(compLinearMap f₁ g + compLinearMap f₂ g) x✝
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.362901
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.362931
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.363319
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
ι' : Type ?u.363710
ι'' : Type ?u.363713
M₂ : Type u_5
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.363746
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f₁ f₂ : AlternatingMap R M N ι
g : M₂ →ₗ[R] M
⊢ compLinearMap (f₁ + f₂) g = compLinearMap f₁ g + compLinearMap f₂ g
ext
no goals
case H
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.362901
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.362931
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.363319
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
ι' : Type ?u.363710
ι'' : Type ?u.363713
M₂ : Type u_5
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.363746
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f₁ f₂ : AlternatingMap R M N ι
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ↑(compLinearMap (f₁ + f₂) g) x✝ = ↑(compLinearMap f₁ g + compLinearMap f₂ g) x✝
simp only [compLinearMap_apply, add_apply]