OAI/Analysis/KadisonKastler/FixedFactorPublishedInputs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Published inputs for the fixed-factor preparation argument

  1. structure OAI.KadisonKastler.FixedFactorPublishedInputs line 18

    Source documentation

    Every field refers to a separately documented published result. There is no stability, preparation or fixed-factor conclusion among these assumptions.

    structure FixedFactorPublishedInputs : Prop extends ModularCorePublishedInputs.{u} where
…
  2. theorem OAI.KadisonKastler.TwoRatioProductModel.typeIII1_of_published line 26