Math 2.0

statement corollary

Constant multiple rule

Statement

Let ff be a real function on an open interval II, differentiable at a∈Ia \in I, and let cc be a real number. Then cfc f is differentiable at aa, and (cf)′(a)=cf′(a)(c f)'(a) = c f'(a).

Remarks

It is the case β=0\beta = 0 of the linearity of differentiation. For example, (5x2)′=10x(5 x^2)' = 10 x. Mathlib states it as deriv_const_mul.

Explanations

L1 human

Stretching a graph vertically by a factor cc multiplies all its slopes by cc.

What this node needs for W1
  • an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a node is. They do not measure its truth.

What this needs

To read this node, read these 10 nodes in this order. The foundations come first, and the list ends with this node.

Each node uses the nodes above it. The colour of the bar on a box shows the evidence level, and the box also gives it as text. The list below has the same nodes.
  • no evidence level
  1. Limit point of a set definition
  2. Sequence definition
  3. Limit of a function definition
  4. Real sequence definition
  5. Derivative definition
  6. Limit of a sequence definition
  7. Epsilon-N definition of the limit of a sequence statement
  8. Limit of a sum of sequences statement
  9. Linearity of differentiation statement
  10. Constant multiple rule statement

Sources

  1. Web https://en.wikipedia.org/wiki/Linearity_of_differentiation, Constant coefficient