OAI/Analysis/OperatorAlgebra/PointwiseTomita.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Commutation under the amplified Tomita conjugation.

  1. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_mul line 16

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

  2. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_commute line 24
  3. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_commute_iff line 30
  4. lemma OAI.WeakPureInfiniteness.pointwiseTomita_commute_iff line 39