OAI/Analysis/KadisonKastler/PositiveReferenceModular.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The polar conjugation is unchanged at positive cyclic references

The old quadratic cone supplies positivity at the new reference. The proved uniqueness theorem then identifies its constructed conjugation.

  1. theorem OAI.KadisonKastler.positiveCone_quadratic_complex_nonneg line 25
  2. theorem OAI.KadisonKastler.positiveCone_polar_conjugation line 44