R : Type u_4
inst✝¹⁵ : Semiring R
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N : Type u_2
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
P : Type ?u.449922
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.449952
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.450340
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.450731
ι'' : Type ?u.450734
M₂ : Type ?u.450737
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.450767
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
f f' : AlternatingMap R M N ι
g g₂ : AlternatingMap R M N' ι
g' : AlternatingMap R M' N' ι
v : ι → M
v' : ι → M'
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ ↑f (v ∘ ↑(Equiv.swap i j)) + ↑f v = 0
R : Type u_4
inst✝¹⁵ : Semiring R
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N : Type u_2
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
P : Type ?u.449922
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.449952
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.450340
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.450731
ι'' : Type ?u.450734
M₂ : Type ?u.450737
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.450767
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
f f' : AlternatingMap R M N ι
g g₂ : AlternatingMap R M N' ι
g' : AlternatingMap R M' N' ι
v : ι → M
v' : ι → M'
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ ↑f v + ↑f (v ∘ ↑(Equiv.swap i j)) = 0
rw [add_comm]
no goals
R : Type u_4
inst✝¹⁵ : Semiring R
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N : Type u_2
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
P : Type ?u.449922
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.449952
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.450340
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.450731
ι'' : Type ?u.450734
M₂ : Type ?u.450737
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.450767
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
f f' : AlternatingMap R M N ι
g g₂ : AlternatingMap R M N' ι
g' : AlternatingMap R M' N' ι
v : ι → M
v' : ι → M'
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ ↑f (v ∘ ↑(Equiv.swap i j)) + ↑f v = 0
exact f.map_swap_add v hij