pith. machine review for the scientific record. sign in
theorem proved term proof

cosh_eq_one_iff

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  34private theorem cosh_eq_one_iff (t : ℝ) : Real.cosh t = 1 ↔ t = 0 := by

proof body

Term-mode proof.

  35  constructor
  36  · intro h
  37    by_contra hne
  38    have hgt : 1 < Real.cosh t := Real.one_lt_cosh.mpr hne
  39    linarith
  40  · intro h
  41    simp [h]
  42
  43/-- The abstract zero-location composition law needed by Vector C. -/

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.