case a
R : Type u_2
inst✝¹² : Semiring R
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.719894
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.719924
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.719954
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_4
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_1
ι' : Type ?u.720733
ι'' : Type ?u.720736
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : AlternatingMap R M N' ι
⊢ ↑(↑MultilinearMap.alternatization ↑a) = ↑(Nat.factorial (Fintype.card ι) • a)
R : Type u_2
inst✝¹² : Semiring R
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.719894
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.719924
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.719954
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_4
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_1
ι' : Type ?u.720733
ι'' : Type ?u.720736
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : AlternatingMap R M N' ι
⊢ ↑MultilinearMap.alternatization ↑a = Nat.factorial (Fintype.card ι) • a
apply AlternatingMap.coe_injective
no goals
case a
R : Type u_2
inst✝¹² : Semiring R
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.719894
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.719924
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.719954
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_4
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_1
ι' : Type ?u.720733
ι'' : Type ?u.720736
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : AlternatingMap R M N' ι
⊢ ↑(↑MultilinearMap.alternatization ↑a) = ↑(Nat.factorial (Fintype.card ι) • a)
simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
  smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
  ← coe_multilinearMap, coe_smul]