IndisputableMonolith.Mathematics.Pi

declarations in this module (18)

• def octagonPerimeter L55
• def piFromOctagon L57
• theorem octagon_approximates_pi L59
• def inscribedPerimeter L79
• def circumscribedPerimeter L82
• theorem octagon_bounds L90
• theorem pi_over_4_fundamental L104
• theorem pi_from_eight_quarters L117
• theorem cos_pi_5_is_phi_2 L130
• theorem sin_pi_10_from_phi L137
• def goldenAngle L213
• def piSeries L224
• def leibniz_8_terms L240
• theorem leibniz_8_approximates L243
• def piInPhysics L259
• theorem pi_transcendence L276
• def rsPerspective L292
• structure PiFalsifier L305