Theorems · Theorem · complex analysis
Real.tanh_eq
∀ (x : ℝ), Real.tanh x = (Real.exp x - Real.exp (-x)) / (Real.exp x + Real.exp (-x))
The definition of tanh in terms of exp.
- Defined in
- Mathlib.Analysis.Complex.Trigonometric
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Real.expstatement and proof · cited by 871
- two_ne_zeroproof · cited by 251
- Real.coshproof · cited by 119
- Real.tanhstatement · cited by 19
- div_div_div_cancel_right₀proof · cited by 6
- Real.sinh_eqproof · cited by 5
- Real.tanh_eq_sinh_div_coshproof · cited by 5
- Real.cosh_eqproof · cited by 5
Cited by3
Results whose statement or proof uses this declaration.
- Real.neg_one_lt_tanhproof · cited by 1
- Real.tanh_lt_oneproof · cited by 1
- Real.artanh_tanhproof · cited by 0