structure definition def or abbrev

`LogicComplex`

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

formal statement (Lean)

  27structure LogicComplex where
  28  re : LogicReal
  29  im : LogicReal
  30
  31namespace LogicComplex
  32
  33/-- Transport a recovered complex number to Mathlib's complex line. -/

used by (27)

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 in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
fromComplex_toComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
logicComplex_recovered_from_mathlib in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
ofLogicRat in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
ofLogicReal in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_add in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_div in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_im in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_inv in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_mul in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_neg in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_one in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_re in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_sub in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_zero in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
logicCompletedRiemannZeta in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
logicCompletedRiemannZeta_one_sub in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
LogicComplexAnalyticSubstrateCert in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
logicRiemannZeta in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
logicRiemannZeta_eulerProduct_tendsto in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
toComplex_re_eq 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

depends on (1)

Lean names referenced from this declaration's body.

LogicReal in IndisputableMonolith.Foundation.RealsFromLogic decl_use