Model.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.HasScalarCenter line 14
Source documentation
A concrete factor has scalar center.
Also declared: ComparatorChallenges/FiniteFactor.lean:14 (same declaration text).
```
def HasScalarCenter (M : VonNeumannAlgebra H) : Prop :=
…
```
def OAI.FiniteFactor.IsFiniteAlgebra line 18
Source documentation
Finiteness: every isometry in the algebra is unitary.
Also declared: ComparatorChallenges/FiniteFactor.lean:18 (same declaration text).
```
def IsFiniteAlgebra (M : VonNeumannAlgebra H) : Prop :=
…
```
def OAI.FiniteFactor.HasNoMinimalProjection line 22
Source documentation
No nonzero projection is minimal, excluding matrix factors.
Also declared: ComparatorChallenges/FiniteFactor.lean:22 (same declaration text).
```
def HasNoMinimalProjection (M : VonNeumannAlgebra H) : Prop :=
…
```
def OAI.FiniteFactor.HasSeparablePredual line 27
Source documentation
A separable Banach space whose dual is conjugate-linearly isometric to M.
Also declared: ComparatorChallenges/FiniteFactor.lean:27 (same declaration text).
```
def HasSeparablePredual (M : VonNeumannAlgebra H) : Prop :=
…
```
def OAI.FiniteFactor.MainTarget line 32
Also declared: ComparatorChallenges/FiniteFactor.lean:32 (same declaration text).