module module

`IndisputableMonolith.Constants.EulerMascheroni`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (12)

structure or L16
abbrev gamma L28
theorem gamma_pos L31
theorem gamma_lt_two_thirds L35
theorem gamma_numerical_bounds L39
theorem euler_mascheroni_bounds L53
theorem euler_mascheroni_implies_pos L57
theorem euler_mascheroni_implies_ne_zero L62
theorem gamma_irrational_conjecture L75
theorem gamma_bounds_optimal L81
theorem gamma_rs_prediction L92
theorem gamma_gap_analysis L103