theorem proved term proof

`cosh_no_real_zeros`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  75theorem cosh_no_real_zeros (t : ℝ) : 1 ≤ Real.cosh t := by

proof body

Term-mode proof.

  76  have h := Real.cosh_pos t
  77  have h2 := Cost.cosh_quadratic_lower_bound t
  78  linarith [sq_nonneg t]
  79
  80/-- cosh(0) = 1: the unique real minimum. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

j_positive_off_fixed_point in IndisputableMonolith.NumberTheory.PrimeLedgerStructure decl_use

depends on (2)

Lean names referenced from this declaration's body.

cosh_quadratic_lower_bound in IndisputableMonolith.Cost decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use