Documentation

Lean 4 Proof

theorem alpha_duality_involution {σ : ℝ} (hσ : σ ≠ 0) (hσ1 : σ ≠ 1) :
    alphaOfSigma (σ / (σ - 1)) = -alphaOfSigma σ := by
  unfold alphaOfSigma
  have h1 : σ - 1 ≠ 0 := sub_ne_zero.mpr hσ1
  have h2 : σ / (σ - 1) ≠ 0 := div_ne_zero hσ h1
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:90

Module Section

### The Boltzmann-Escort Identification

In the same file