IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField

declarations in this module (22)

• theorem subfield_closure_countable_of_countable L55
• theorem subfield_closure_countable_of_finite L65
• def w8 L72
• def alphaInv L76
• def rsConstants L80
• def rsField L86
• theorem rsConstants_finite L89
• theorem rsConstants_countable L93
• theorem rsField_countable L97
• theorem rsField_mem_phi L100
• theorem rsField_mem_pi L103
• theorem rsField_mem_e L106
• theorem rsField_mem_alphaInv L109
• theorem rsField_proper L114
• theorem rs_physics_below_continuum L123
• theorem rsField_phi_zpow L143
• theorem rsField_natCast L147
• theorem rsField_eight_tick L151
• theorem rsField_dimension L155
• theorem rsField_mass_ladder L161
• theorem rsField_extend_stays_countable L168
• theorem rs_scaffold_below_continuum L176