Documentation

Lean 4 Proof

def SubstituteRegime (ρ : ℝ) : Prop := 1 < ρ

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:245

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file