module
module
IndisputableMonolith.NumberTheory.DirectedEulerLedger
show as:
view Lean formalization →
used by (1)
depends on (2)
declarations in this module (10)
-
abbrev
PrimeSupport -
theorem
primeSupport_directed -
theorem
primeEulerEvent_mem_sensorEulerLedger_of_subset -
theorem
reciprocal_primeEulerEvent_mem_sensorEulerLedger_of_subset -
structure
DirectedEulerLedgerSystem -
def
concreteDirectedEulerLedgerSystem -
theorem
concreteDirectedEulerLedgerSystem_union_contains -
structure
EulerLedgerOntologyInterface -
def
concreteEulerLedgerOntologyInterface -
theorem
concreteEulerLedgerOntologyInterface_exists