module module

`IndisputableMonolith.Foundation.ComplexFromLogic`

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

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

IndisputableMonolith.Foundation.LogicComplexCompat module_import
IndisputableMonolith.Foundation.RecoveredTowerAxiomAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.RealsFromLogic module_import

declarations in this module (22)

structure LogicComplex L27
def toComplex L34
def fromComplex L38
theorem toComplex_re L42
theorem toComplex_im L45
theorem toComplex_fromComplex L48
theorem fromComplex_toComplex L52
def equivComplex L59
theorem eq_iff_toComplex_eq L66
theorem toComplex_zero L86
theorem toComplex_one L89
theorem toComplex_add L92
theorem toComplex_neg L96
theorem toComplex_sub L100
theorem toComplex_mul L104
theorem toComplex_inv L108
theorem toComplex_div L112
def ofLogicReal L117
theorem toComplex_ofLogicReal L121
def ofLogicRat L127
theorem toComplex_ofLogicRat L130
theorem logicComplex_recovered_from_mathlib L136