OAI/Analysis/FiniteFactor/Diffuse/TracePowers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nonhyperlinear.Diffuseness.trace_defect_pow line 12

   Source documentation

   Cyclicity equates every polynomial defect moment; no spectral assumption is used.

   theorem trace_defect_pow {A:Type*} [Ring A] [Algebra ℂ A]
       (f:A→ₗ[ℂ]ℂ) (hf:∀a b,f (a*b)=f (b*a)) (a b:A) (n:ℕ) :
       f ((1-a*b)^n)=f ((1-b*a)^n) := by
   …