OAI/Analysis/PureInfiniteness/UltrapowerGramCuts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The row with an exact cut diagonal Gram matrix used in KR02 Remark 7.5. The original positive elements may be arbitrary elements of the norm ultrapower, as required when iterating the abelianization argument.

  1. theorem OAI.WeakPureInfiniteness.ultrapower_cut_gram_row line 20