Documentation

Lean 4 Proof

theorem curvatureK_eq_zero_of_rho_one {J : ℕ} :
    curvatureK J 1 = 0 := by
  simp [curvatureK]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:152

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file