module module

`IndisputableMonolith.PhiSupport.Alternatives`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RecogSpec.PhiSelectionCore module_import

declarations in this module (6)

theorem sqrt2_fails_selection L22
theorem sqrt3_fails_selection L43
theorem sqrt5_fails_selection L65
theorem pi_fails_selection L86
theorem e_fails_selection L109
theorem common_constants_fail_selection L190