module
module
IndisputableMonolith.Superhuman.Core
show as:
view Lean formalization →
used by (2)
depends on (2)
declarations in this module (15)
-
inductive
PowerClass -
inductive
Power -
def
powerClass -
def
allPowers -
theorem
powerCount_eq_27 -
theorem
accessible_count_eq_23 -
theorem
constrained_count_eq_4 -
theorem
classA_count -
theorem
classB_count -
theorem
classC_count -
theorem
classD_count -
theorem
classE_count -
inductive
ConstraintReason -
def
constraintReason -
theorem
constrained_has_reason