R : Type u_4
inst✝¹⁶ : Semiring R
M : Type u_3
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
N : Type ?u.482812
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module R N
P : Type ?u.482842
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : Module R P
M' : Type ?u.482872
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
N' : Type u_2
inst✝⁷ : AddCommGroup N'
inst✝⁶ : Module R N'
ι : Type u_1
ι' : Type ?u.483651
ι'' : Type ?u.483654
M₂ : Type ?u.483657
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
M₃ : Type ?u.483687
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 ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ ↑g v = (↑Equiv.Perm.sign σ * ↑Equiv.Perm.sign σ) • ↑g v
R : Type u_4
inst✝¹⁶ : Semiring R
M : Type u_3
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
N : Type ?u.482812
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module R N
P : Type ?u.482842
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : Module R P
M' : Type ?u.482872
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
N' : Type u_2
inst✝⁷ : AddCommGroup N'
inst✝⁶ : Module R N'
ι : Type u_1
ι' : Type ?u.483651
ι'' : Type ?u.483654
M₂ : Type ?u.483657
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
M₃ : Type ?u.483687
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 ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ ↑g v = ↑Equiv.Perm.sign σ • ↑g (v ∘ ↑σ)
rw [g.map_perm, smul_smul]
no goals
R : Type u_4
inst✝¹⁶ : Semiring R
M : Type u_3
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
N : Type ?u.482812
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module R N
P : Type ?u.482842
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : Module R P
M' : Type ?u.482872
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
N' : Type u_2
inst✝⁷ : AddCommGroup N'
inst✝⁶ : Module R N'
ι : Type u_1
ι' : Type ?u.483651
ι'' : Type ?u.483654
M₂ : Type ?u.483657
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
M₃ : Type ?u.483687
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 ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ ↑g v = (↑Equiv.Perm.sign σ * ↑Equiv.Perm.sign σ) • ↑g v
simp