OAI/Analysis/KadisonKastler/FreeHaarTwists.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Adjoint and left twists of the constructed free Haar unitary

  1. theorem OAI.KadisonKastler.haarPower_star line 14

    Source documentation

    Taking the adjoint negates every Haar exponent.

    theorem haarPower_star (u : unitary B) (k : ℤ) :
    haarPower (star u) k = haarPower u (-k) := by
…

    Mentions: OAI.KadisonKastler.haarPower

  2. theorem OAI.KadisonKastler.FreeHaarMoments.star line 22
  3. theorem OAI.KadisonKastler.FreeHaarMoments.mul_left line 33

    Source documentation

    Multiplication on the left by a unitary in the base preserves the same free Haar moment identities.

    theorem mul_left (h : FreeHaarMoments τ A s) (U : unitary B) (hU : (U : B) ∈ A) :
    FreeHaarMoments τ A (U * s) := by
…

    Mentions: OAI.KadisonKastler.FreeHaarMoments