Documentation

Lean 4 Proof

theorem qExp_zero (q : ℝ) : qExp q 0 = 1 := by
  simp only [qExp]
  split_ifs with h
  · exact Real.exp_zero
  · simp [rpow_def_of_pos one_pos]

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:48

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file