IndisputableMonolith.Meta.ConstructiveNote

declarations in this module (15)

• class Computable L53
• theorem pi_computable L71
• theorem phi_computable L88
• lemma two_zpow_pos L91
• instance rational_computable L141
• theorem computable_neg L150
• theorem computable_add L166
• theorem computable_sub L199
• theorem computable_mul L214
• theorem computable_div L230
• theorem computable_pow L237
• theorem computable_log L261
• theorem alpha_seed_computable L269
• theorem log_phi_computable L277
• theorem curvature_computable L283