Lean 4 (v4.34.1 / Mathlib) formalization of noncommutative information geometry, Peirce-Weyl units, Drazin-Moore-Penrose spectral splittings, Jordan-Lie operator algebras, and categorical inductive colimits.
theorem-proving category-theory formal-verification operator-algebras grassmannian information-geometry weyl-group drazin-inverse lean4 moore-penrose-inverse mathlib4 noncommutative-geometry jordan-algebra peirce-decomposition inductive-colimits
-
Updated
Nov 11, 2026 - Lean