OAI/Analysis/FreeWords/PartialUnitaryChain.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.KKLocalPatching.PartialUnitary.directed_power_cauchyline 30 - theorem
OAI.KKLocalPatching.PartialUnitary.directed_limitline 52