Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:242

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file