English
Let a be a positive ordinal. The derivative of the multiplication by a at a fixed point b is given by a^ω multiplied by b, describing how growth scales under multiplication by a in the ordinal fixed-point framework.
Русский
Пусть a — положительный ординал. Производная умножения на a в точке фиксированной точки b задаётся как a^ω · b, отражая рост в рамках фикс-пунктной арифметики по ординалам.
LaTeX
$$$ (0 < a) \\rightarrow \\deriv(a \\cdot \\cdot) b = a^\\omega \\cdot b $$$
Lean4
theorem deriv_mul_eq_opow_omega0_mul {a : Ordinal.{u}} (ha : 0 < a) (b) : deriv (a * ·) b = a ^ ω * b :=
by
revert b
rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) (isNormal_mul_right (opow_pos ω ha))]
refine ⟨?_, fun c h => ?_⟩
· dsimp only; rw [deriv_zero_right, nfp_mul_zero, mul_zero]
· rw [deriv_succ, h]
exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))
