OAI/Analysis/KadisonKastler/PointedOperationsAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Assembling the pointed-product operations

The sum and reindexing clauses are proved from the finite-site identities. Only the concrete lambda product construction remains as an argument here.

  1. theorem OAI.KadisonKastler.publishedPointedMatrixOperations_of_powers line 21