English
If a ≠ 0, IsMIntegralCurveAt γ v t0 is equivalent to IsMIntegralCurveAt (γ ∘ (· * a)) (a • v) (t0 / a). This shows how integral curves transform under nonzero time rescaling around t0.
Русский
При a ≠ 0 интегральная кривая трансформируется как IsMIntegralCurveAt(γ ∘ (· * a)) (a•v) (t0 / a).
LaTeX
$$$IsMIntegralCurveAt(\\gamma, v, t_0) \\iff IsMIntegralCurveAt(\\gamma \\circ (\\cdot * a), a \\cdot v, t_0 / a)$$$
Lean4
theorem isMIntegralCurveAt_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
IsMIntegralCurveAt γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ (· * a)) (a • v) (t₀ / a) :=
by
refine ⟨fun hγ ↦ hγ.comp_mul_ne_zero ha, fun hγ ↦ ?_⟩
convert hγ.comp_mul_ne_zero (inv_ne_zero ha)
· ext t
simp only [Function.comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
· simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]
· simp only [div_inv_eq_mul, div_mul_cancel₀ _ ha]
