OAI/Analysis/Commutator/FiniteCancellation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.IsFiniteAlgebra line 18
2. lemma OAI.Kadison.PartialIsometryOrder.IsFiniteAlgebra.coisometry line 21
3. lemma OAI.Kadison.PartialIsometryOrder.finite_corner_cancel line 25
4. lemma OAI.Kadison.PartialIsometryOrder.Link.extend_initial line 57
5. lemma OAI.Kadison.PartialIsometryOrder.Link.extend_final line 64
6. theorem OAI.Kadison.PartialIsometryOrder.finite_unitary_extension line 73