no goals
R : Type ?u.1240826
inst✝²¹ : Semiring R
M : Type ?u.1240832
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.1240864
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.1240894
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.1240924
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.1241312
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.1241700
ι' : Type ?u.1241703
ι'' : Type ?u.1241706
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
⊢ ↑alternatization (domCoprod ↑a ↑b) =
    (Nat.factorial (Fintype.card ιa) * Nat.factorial (Fintype.card ιb)) • AlternatingMap.domCoprod a b
rw [MultilinearMap.domCoprod_alternization, coe_alternatization, coe_alternatization, mul_smul,
  ← AlternatingMap.domCoprod'_apply, ← AlternatingMap.domCoprod'_apply,
  ← TensorProduct.smul_tmul', TensorProduct.tmul_smul,
  LinearMap.map_smul_of_tower AlternatingMap.domCoprod',
  LinearMap.map_smul_of_tower AlternatingMap.domCoprod']