lemma
proved
term proof
cosh_eq_one_iff
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)
102private lemma cosh_eq_one_iff (t : ℝ) : cosh t = 1 ↔ t = 0 := by
proof body
Term-mode proof.
103 constructor
104 · intro h
105 by_contra hne
106 exact absurd h (ne_of_gt ((one_lt_cosh).mpr hne))
107 · intro h; rw [h, cosh_zero]
108
109/-- J̃(lam, δ) = 0 iff δ is an integer, for lam ≠ 0. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
cosh_eq_one_iff
in IndisputableMonolith.NumberTheory.ZeroCompositionInterface
decl_use