OAI/Analysis/JiangSu/CentralSequences/NormUltrapowerUnitaryLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NormUltra.QuotientAlgebra.boundedUnitary line 18
2. theorem OAI.NormUltra.QuotientAlgebra.unitary_representative line 30