RepresentedIdealSeparation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Product pure-state ideal separation for a fixed factor representation. The only nuclearity input here concerns its actual represented left image.

theorem OAI.WeakPureInfiniteness.productPure_separates_ideals_of_representation line 21