def definition def or abbrev

`fromComplex`

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

formal statement (Lean)

  38def fromComplex (z : ℂ) : LogicComplex where
  39  re := fromReal z.re

Definition body.

  40  im := fromReal z.im
  41

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

eq_iff_toComplex_eq in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
equivComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
fromComplex_toComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
logicComplex_recovered_from_mathlib in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_fromComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
logicCompletedRiemannZeta_fromComplex in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
logicCompletedRiemannZeta_one_sub in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
LogicComplexAnalyticSubstrateCert in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
logicRiemannZeta_fromComplex in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
logic_completed_zeta_functional_equation in IndisputableMonolith.NumberTheory.ZetaFromTheta decl_use
logic_completed_zeta_functional_equation_from_theta in IndisputableMonolith.NumberTheory.ZetaFromTheta decl_use
ZetaFromThetaPhase4Cert in IndisputableMonolith.NumberTheory.ZetaFromTheta decl_use

Lean names referenced from this declaration's body.