module module

`IndisputableMonolith.Cost.TraceRationalExponent`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cost.RealCharacterFactorization module_import

declarations in this module (8)

theorem no_rational_sqrt_five L55
theorem no_rational_character_at_trace_three L74
theorem golden_square_has_trace_three L87
theorem pow_eq_coords L104
theorem rat_of_trace_rat_of_pow_rat L150
theorem int_of_rat_exponent_of_trace_rat L175
def SixExponentialsTraceInput L237
theorem exponent_is_positive_integer L247