lemma other other

`CoshAddIdentity_implies_DirectCoshAdd`

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

formal statement (Lean)

  38lemma CoshAddIdentity_implies_DirectCoshAdd (F : ℝ → ℝ)
  39  (h : CoshAddIdentity F) :
  40  DirectCoshAdd (G F) := h

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

H_dAlembert_of_composition in IndisputableMonolith.Cost.AczelClassification decl_use
composition_law_forces_reciprocity in IndisputableMonolith.Cost.ContDiffReduction decl_use
washburn_uniqueness_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use
washburn_uniqueness in IndisputableMonolith.Cost.FunctionalEquation decl_use
washburn_uniqueness_aczel in IndisputableMonolith.Cost.FunctionalEquation decl_use
washburn_uniqueness_aczel in IndisputableMonolith.Cost.FunctionalEquationAczel decl_use
T5_uniqueness_complete in IndisputableMonolith.CostUniqueness decl_use

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
CoshAddIdentity in IndisputableMonolith.Cost.FunctionalEquation decl_use
DirectCoshAdd in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use