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

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : IsScalarTower ℝ 𝕜 G
inst✝² : SMulCommClass ℝ 𝕜 G
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra ℝ 𝔸
a : 𝔸
⊢ HasTemperateGrowth fun x => x / a
Tactic:
simp_rw [div_eq_mul_inv]
State after:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : IsScalarTower ℝ 𝕜 G
inst✝² : SMulCommClass ℝ 𝕜 G
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra ℝ 𝔸
a : 𝔸
⊢ HasTemperateGrowth fun x => x * a⁻¹

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : IsScalarTower ℝ 𝕜 G
inst✝² : SMulCommClass ℝ 𝕜 G
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra ℝ 𝔸
a : 𝔸
⊢ HasTemperateGrowth fun x => x * a⁻¹
Tactic:
exact hasTemperateGrowth_mul_const a⁻¹
State after:
no goals