OAI/Analysis/OperatorAlgebra/AntiunitaryOperatorIdentities.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Multiplication and adjoints under an actual involutive antiunitary.

  1. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_mul line 13

    Distinct definitions of this name: OAI/Analysis/OperatorAlgebra/PointwiseTomita.lean:16 (different declaration text). Qualify references as OAI.WeakPureInfiniteness.antiunitaryConjugate_mul@path.

  2. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_star line 21
  3. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_isStarProjection line 37