R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
i : ι → ι
h : Injective i
⊢ (↑f fun i_1 => ↑e (i i_1)) = ↑(↑f ↑e • Basis.det e) fun i_1 => ↑e (i i_1)
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
⊢ f = ↑f ↑e • Basis.det e
refine' Basis.ext_alternating e fun i h => _
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i (_ : Bijective i)
⊢ (↑f fun i_1 => ↑e (i i_1)) = ↑(↑f ↑e • Basis.det e) fun i_1 => ↑e (i i_1)
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
i : ι → ι
h : Injective i
⊢ (↑f fun i_1 => ↑e (i i_1)) = ↑(↑f ↑e • Basis.det e) fun i_1 => ↑e (i i_1)
let σ : Equiv.Perm ι := Equiv.ofBijective i (Finite.injective_iff_bijective.1 h)
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i (_ : Bijective i)
⊢ ↑f (↑e ∘ ↑σ) = ↑(↑f ↑e • Basis.det e) (↑e ∘ ↑σ)
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i (_ : Bijective i)
⊢ (↑f fun i_1 => ↑e (i i_1)) = ↑(↑f ↑e • Basis.det e) fun i_1 => ↑e (i i_1)
change f (e ∘ σ) = (f e • e.det) (e ∘ σ)
no goals
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2583010
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : AlternatingMap R M R ι
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i (_ : Bijective i)
⊢ ↑f (↑e ∘ ↑σ) = ↑(↑f ↑e • Basis.det e) (↑e ∘ ↑σ)
simp [AlternatingMap.map_perm, Basis.det_self]