Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing (ForML/HasTemperateGrowth.lean)

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
⊢ HasTemperateGrowth fun x => ContinuousMultilinearMap.mkPiRing ℝ ι x
Tactic:
simp only [← ContinuousMultilinearMap.mkPiRingL_apply]
State after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
⊢ HasTemperateGrowth fun x => (ContinuousMultilinearMap.mkPiRingL ℝ F) x

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
⊢ HasTemperateGrowth fun x => (ContinuousMultilinearMap.mkPiRingL ℝ F) x
Tactic:
exact hasTemperateGrowth_clm _
State after:
no goals