Documentation

Lean 4 Proof

theorem qSum_comm (q a b : ℝ) : qSum q a b = qSum q b a := by
  simp [qSum]; ring

Dependency Graph

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:98

Module Section

Theorem 2: Tsallis Uniqueness (Paper 2, Section 3.1)

In the same file