unfold Distribution.extAction'
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => Distribution.extAction' (y u) φ
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => (y u).extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)