RationalComplexCore.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

All coefficient identities can be made simultaneous on this countable core before bounded maps are extended to the whole Hilbert space.

instance OAI.KadisonKastler.(instance at line 23) line 23
Source documentation
The canonical rational scalar action inherited from the complex action.
```
instance (priority := 100) rationalCoreModule : Module ℚ H :=
…
```
structure OAI.KadisonKastler.RationalComplexCore line 28
Source documentation
A dense rational subspace on which all complex-linearity tests remain countable, since multiplication by i preserves the subspace.
```
structure RationalComplexCore where
…
```
theorem OAI.KadisonKastler.exists_rationalComplexCore line 35
Source documentation
Every separable complex normed space admits such a core.
```
theorem exists_rationalComplexCore [SeparableSpace H] : Nonempty (RationalComplexCore H) := by
…
```
Mentions: OAI.KadisonKastler.RationalComplexCore
def OAI.KadisonKastler.RationalComplexCore.mulI line 64
Source documentation
Multiplication by i as an endomorphism of the countable core.
```
def mulI : C.space →ₗ[ℚ] C.space where
…
```
theorem OAI.KadisonKastler.RationalComplexCore.coe_mulI line 70