def definition def or abbrev

`functionalReflection`

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

formal statement (Lean)

  29def functionalReflection (ρ : ℂ) : ℂ :=

Definition body.

  30  1 - ρ
  31
  32/-- Reflection across the line `Re(s) = 1/2`, composed with conjugation. -/

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

functionalEquation_gives_pairing_invariants in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
xi_reflection_invariant in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
zeroDefectSet_reflection_invariant in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
zeroDeviationSet_neg_closed in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
zero_pairing_under_critical_reflection in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
zero_pairing_under_reflection in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
PureVectorCDoublingData in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
toyXi_reflection in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
functionalReflection_re in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_invariant_under_functional_reflection in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDeviation_functionalReflection in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use