statement proposition
cosh^2 - sinh^2 = 1
Statement
For every real ,
Remarks
The left side factors as .
So the point lies on the right branch of the hyperbola .
Dividing by gives . Mathlib states the identity as Real.cosh_sq_sub_sinh_sq.
Explanations
L1 human
This is the hyperbolic version of , with a minus sign. It follows directly from the definitions with and .
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 28 nodes in this order. The foundations come first, and the list ends with this node.
- no evidence level
- Sequence definition
- Real sequence definition
- Bounded sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Series definition
- Sum of a finite geometric series statement
- Monotone convergence theorem for sequences statement
- Convergent sequence definition
- Squeeze theorem statement
- Partial sum definition
- Power series definition
- The sequence r^n tends to zero for |r| < 1 example
- Radius of convergence definition
- Convergent series definition
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Absolute convergence definition
- Sum of a series definition
- Comparison test statement
- Geometric series example
- Ratio test statement
- Ratio formula for the radius of convergence statement
- The exponential series has infinite radius of convergence statement
- Exponential function definition
- Hyperbolic cosine definition
- Hyperbolic sine definition
- cosh^2 - sinh^2 = 1 statement
What depends on this
1 node uses this node, directly or through other nodes.
- Derivatives of the hyperbolic functions 07T2TKGZ4J
Sources
- Web https://en.wikipedia.org/wiki/Hyperbolic_functions, Useful relations
What links here
Used by
- Derivatives of the hyperbolic functions 07T2TKGZ4J