module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Kernel
show as:
view Lean formalization →
used by (2)
depends on (30)
-
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FormalSystem -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Inevitability -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceTriangle -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceVerifierTriangle -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Quotient -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealBoundednessModulus -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedFieldPromoted -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompletion -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealMulBoundedContinuity -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealNullSetoid -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealOrderCongruence -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealProductContinuity -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RecognizerBridge -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceLogic