OAI/Analysis/PureInfiniteness/FiniteFamilyAbelianization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite iteration of the one-coefficient compression, as in the first paragraph of KR02 Lemma 7.12. Previously compressed coefficients are included among the commuting elements fixed by the next compression.

  1. lemma OAI.WeakPureInfiniteness.compression_product line 15
  2. theorem OAI.WeakPureInfiniteness.ultrapower_finite_family_abelianization line 24