OAI/Analysis/KadisonSimilarity/FreeProduct/FiniteFactorFreeness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constructed irreducible matrix source supplies the free position required by every separably acting finite factor.

  1. theorem OAI.KadisonSimilarity.FiniteFactorPresentation.freePosition line 21
  2. theorem OAI.KadisonSimilarity.publishedFactorCases line 65

    Source documentation

    The three structural factor alternatives have local free-position data.

    theorem publishedFactorCases [Nontrivial H]
    (hfactor : ∀ a : P.toStarSubalgebra, (∀ b, a * b = b * a) →
      ∃ c : ℂ, a = algebraMap ℂ P.toStarSubalgebra c) :
    PublishedFactorCasesInput P := by
…

    Mentions: OAI.KadisonSimilarity.PublishedFactorCasesInput