OAI/Analysis/FreeWords/MixedScaling.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.KKLocalPatching.mixedValueline 18 - def
OAI.KKLocalPatching.scaledMixedline 21 - theorem
OAI.KKLocalPatching.mixedValue_scaledline 24 - theorem
OAI.KKLocalPatching.mixedValue_restoreline 34 - theorem
OAI.KKLocalPatching.norm_trace_scaledline 39