OAI/Analysis/PureInfiniteness/CompressedCoefficientAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A compressed coefficient belongs to the algebra generated by the four compressed positive parts. This keeps the commutative algebra in the original nonunital ambient algebra.

  1. def OAI.WeakPureInfiniteness.compressedParts line 16
  2. lemma OAI.WeakPureInfiniteness.compressedParts_nonneg line 19
  3. lemma OAI.WeakPureInfiniteness.compression_mem_of_parts line 23
  4. lemma OAI.WeakPureInfiniteness.compression_mem_coefficientAlgebra line 30
  5. lemma OAI.WeakPureInfiniteness.compressedParts_algebra_commutative line 36