OAI/Analysis/KadisonKastler/PositiveIsometryPullback.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Faithful positive references pulled back from a modular corner

  1. theorem OAI.KadisonKastler.positive_isometry_pullback_separating line 28
  2. theorem OAI.KadisonKastler.positive_isometry_pullback_nonzero line 48
  3. theorem OAI.KadisonKastler.positive_isometry_pullback_normalized line 63