OAI/Analysis/KadisonKastler/PositiveConjugationUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A positive standard conjugation is the constructed polar conjugation

The comparison unitary normalizes the algebra and fixes the reference. Positivity of its core pairing determines it via the bounded middle operator. No state homogeneity or uniqueness of standard forms is assumed.

  1. theorem OAI.KadisonKastler.tomitaPolarConjugation_eq_of_quadratic_positive line 23