IndisputableMonolith.Foundation.DeltaSpine.GoldenIntReal

declarations in this module (26)

• def toReal L40
• theorem toReal_zero L43
• theorem toReal_one L45
• theorem toReal_phi L48
• theorem toReal_psi L52
• theorem toReal_add L55
• theorem toReal_neg L60
• theorem toReal_mul L67
• theorem toReal_eq_zero_iff L75
• theorem toReal_injective L105
• theorem posPair_real_pos L118
• theorem isPos_iff_toReal_pos L156
• theorem t6_bridge L181
• theorem toReal_sub L202
• theorem toReal_two L206
• theorem toReal_phiInv L214
• theorem toReal_phiZpow L220
• theorem toReal_traceZ L235
• theorem traceZ_cosh L242
• theorem jdouble_eq_jcost L260
• theorem t5_bridge L272
• theorem toReal_ratWitness L289
• theorem ratLt_toReal L298
• theorem ratGt_toReal L308
• theorem toReal_phiPow L318
• theorem ladder_ratio_real_brackets L326