AbsorptionFromHalfFlip.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Nonunital absorption through a represented quotient and a connected approximate half-flip of O∞ (Kirchberg, Proposition 4.4 and Remark 4.6).

theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption_from_halfFlip line 17