theorem proved term proof

`reciprocal_symmetry_forced`

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

formal statement (Lean)

  48theorem reciprocal_symmetry_forced
  49    (J : ℝ → ℝ)
  50    (h_swap : ∀ x : ℝ, 0 < x → J x = J x⁻¹) :
  51    ∀ x : ℝ, 0 < x → J x = J x⁻¹ := h_swap

proof body

Term-mode proof.

  52
  53/-- **R2 as theorem**: Self-comparison forces J(1) = 0. -/

depends on (3)

Lean names referenced from this declaration's body.

forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
comparison in IndisputableMonolith.StandardModel.StrongCP decl_use