'x' as the default variable. This is the only reasonable choice since we already
always pick 'x' for polynoms.
notation "hvbox(\frac 'd' ('d' ident i) break p)"
right associative with precedence 90
for @{ 'derivative ${default
notation "hvbox(\frac 'd' ('d' ident i) break p)"
right associative with precedence 90
for @{ 'derivative ${default
interpretation "Rderivative" 'derivative \eta.f =
(cic:/matita/demo/power_derivative/derivative.con f).
interpretation "Rderivative" 'derivative \eta.f =
(cic:/matita/demo/power_derivative/derivative.con f).
+*)
+
+notation "hvbox(\frac 'd' ('d' 'x') break p)"
+ right associative with precedence 90
+for @{ 'derivative $p}.
+
+interpretation "Rderivative" 'derivative f =
+ (cic:/matita/demo/power_derivative/derivative.con f).
theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n)*x \sup n.
assume n:nat.
theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n)*x \sup n.
assume n:nat.