case H
R : Type u_2
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.365369
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.365399
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.365787
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.366178
ι'' : Type ?u.366181
M₂ : Type u_5
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.366214
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : Nonempty ι
f : AlternatingMap R M N ι
x✝ : ι → M₂
⊢ ↑(compLinearMap f 0) x✝ = ↑0 x✝
R : Type u_2
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.365369
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.365399
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.365787
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.366178
ι'' : Type ?u.366181
M₂ : Type u_5
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.366214
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : Nonempty ι
f : AlternatingMap R M N ι
⊢ compLinearMap f 0 = 0
ext
case H
R : Type u_2
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.365369
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.365399
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.365787
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.366178
ι'' : Type ?u.366181
M₂ : Type u_5
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.366214
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : Nonempty ι
f : AlternatingMap R M N ι
x✝ : ι → M₂
⊢ ↑f 0 = 0
case H
R : Type u_2
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.365369
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.365399
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.365787
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.366178
ι'' : Type ?u.366181
M₂ : Type u_5
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.366214
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : Nonempty ι
f : AlternatingMap R M N ι
x✝ : ι → M₂
⊢ ↑(compLinearMap f 0) x✝ = ↑0 x✝
simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, zero_apply]
no goals
case H
R : Type u_2
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.365369
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.365399
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.365787
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.366178
ι'' : Type ?u.366181
M₂ : Type u_5
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.366214
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : Nonempty ι
f : AlternatingMap R M N ι
x✝ : ι → M₂
⊢ ↑f 0 = 0
exact map_zero f