IndisputableMonolith.Foundation.LogicRealTranscendentals

declarations in this module (23)

• def sqrtL L26
• def expL L29
• def logL L32
• def rpowL L35
• def piL L38
• def sinL L41
• def cosL L44
• def sinhL L47
• def coshL L50
• theorem toReal_sqrtL L52
• theorem toReal_expL L56
• theorem toReal_logL L60
• theorem toReal_rpowL L64
• theorem toReal_piL L68
• theorem toReal_sinL L71
• theorem toReal_cosL L75
• theorem toReal_sinhL L79
• theorem toReal_coshL L83
• theorem expL_pos L88
• theorem sqrtL_nonneg L93
• theorem expL_logL L98
• theorem logL_expL L105
• theorem coshL_eq_exp L110