module module

`IndisputableMonolith.Cost.RealTraceRoot`

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

def realTraceRoot L17
theorem realTraceRoot_sq_sub_four_nonneg L20
theorem realTraceRoot_one L23
theorem realTraceRoot_ge_one L26
theorem realTraceRoot_pos L31
theorem realTraceRoot_add_inv L34
theorem realTraceRoot_mul L55
theorem larger_trace_of_diff_sq L88
theorem mulDAlembert_duplication L110
theorem mulDAlembert_prod L120
theorem mulDAlembert_diff_sq L134
theorem mulDAlembert_diff_sq_trace L152