WStarAlgebras have Unique Preduals🔗

This is the blueprint of LeanOA, a formalization of operator algebra theory in Lean 4, built on top of Mathlib. Its target is the theorem that a W^*-algebra has a unique predual, along with the C^*/W^*-algebra, locally convex, and ultraweak-topology infrastructure that goal needs.

The numbering of the results below follows Sakai's C*-Algebras and W*-Algebras. The final chapter collects parts of Sakai's development (unitality of W^*-algebras, and the Mackey and strong topologies) that the proof of the main theorem does not need.