OAI/Analysis/PureInfiniteness/AbelianPositiveFixer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The point-fixing input to KR02 Lemma 7.18: every positive element of the separable subalgebra is fixed by an actual abelian-range inner compression.

  1. theorem OAI.WeakPureInfiniteness.abelian_range_compression_fixing_positive line 21