OAI/Analysis/PureInfiniteness/RectangularMaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Applying the unitization embedding to finite rows and columns is contractive. This lets the scalar sample matrices be used without unitalizing the strong pure infiniteness hypothesis.

  1. lemma OAI.WeakPureInfiniteness.rectangularMap_conjTranspose line 21
  2. lemma OAI.WeakPureInfiniteness.rectangularMap_diagonal line 25
  3. lemma OAI.WeakPureInfiniteness.rectangularMap_oneByOne line 33