module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
show as:
view Lean formalization →
used by (10)
-
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitDenseMediant -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitMulPos -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitOrderAddMono -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitZeroLtOne -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrLeftOfBalancedChoiceFree -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrRightOfBalancedChoiceFree -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeMulRightIffOfNonnegFlagOfNotBalancedZeroChoiceFree -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitNonnegFlagMulOfOrbitRightOfNeZeroChoiceFree -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitZeroLeIffNonnegFlagChoiceFree