case H
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_4
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type ?u.744012
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.744042
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.744072
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_2
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.744851
ι'' : Type ?u.744854
N'₂ : Type u_3
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x => M) N'
x✝ : ι → M
⊢ ↑(↑MultilinearMap.alternatization (compMultilinearMap g f)) x✝ =
    ↑(↑(compAlternatingMap g) (↑MultilinearMap.alternatization f)) x✝
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_4
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type ?u.744012
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.744042
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.744072
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_2
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.744851
ι'' : Type ?u.744854
N'₂ : Type u_3
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x => M) N'
⊢ ↑MultilinearMap.alternatization (compMultilinearMap g f) = ↑(compAlternatingMap g) (↑MultilinearMap.alternatization f)
ext
no goals
case H
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_4
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type ?u.744012
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.744042
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.744072
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_2
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.744851
ι'' : Type ?u.744854
N'₂ : Type u_3
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x => M) N'
x✝ : ι → M
⊢ ↑(↑MultilinearMap.alternatization (compMultilinearMap g f)) x✝ =
    ↑(↑(compAlternatingMap g) (↑MultilinearMap.alternatization f)) x✝
simp [MultilinearMap.alternatization_def]