OAI/Analysis/WeakInfiniteness/ElementaryIntertwining.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.minimalPolynomial line 32
2. lemma OAI.WeakPureInfiniteness.minimalPolynomial_denseRange line 35
3. def OAI.WeakPureInfiniteness.ElementaryUnitaryIntertwining line 56
4. lemma OAI.WeakPureInfiniteness.ElementaryUnitaryIntertwining.unitaryFiniteIntertwining line 65
5. lemma OAI.WeakPureInfiniteness.ElementaryUnitaryIntertwining.finiteIntertwining line 137
6. def OAI.WeakPureInfiniteness.oInfinityAbsorptionEquiv_of_elementaryIntertwining line 144