IndisputableMonolith.Foundation.DeltaSpine.GoldenInt

declarations in this module (43)

• structure GoldenInt L52
• def phi L66
• def psi L69
• theorem zero_a L79
• theorem zero_b L80
• theorem one_a L81
• theorem one_b L82
• theorem phi_a L83
• theorem phi_b L84
• theorem psi_a L85
• theorem psi_b L86
• theorem add_a L87
• theorem add_b L88
• theorem neg_a L89
• theorem neg_b L90
• theorem mul_a L91
• theorem mul_b L92
• theorem sub_a L121
• theorem sub_b L126
• def norm L135
• theorem norm_zero L137
• theorem norm_mul L140
• theorem five_dvd_of_five_dvd_sq L147
• theorem sq_ne_five_sq L164
• theorem int_sq_eq_five_sq L192
• theorem norm_eq_zero_iff L201
• theorem mul_eq_zero_iff L226
• theorem phi_sq L239
• theorem psi_sq L242
• theorem phi_ne_psi L245
• theorem golden_factorization L248
• theorem golden_roots L255
• def PosPair L272
• def IsPos L280
• theorem phi_isPos L285
• theorem psi_not_isPos L289
• theorem zero_not_isPos L292
• theorem posPair_trichotomy L298
• theorem posPair_not_neg L336
• theorem isPos_trichotomy L349
• theorem isPos_not_neg L369
• theorem isPos_ne_zero L380
• theorem t6_delta_forced L399