def definition def or abbrev

`toyCompletedXiSurface`

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

formal statement (Lean)

  47def toyCompletedXiSurface : CompletedXiSurface where
  48  xi := toyXi

Definition body.

  49  reflection := toyXi_reflection
  50  conjugation := toyXi_conjugation
  51
  52/-- The toy surface has a zero at `s = 3/4`. -/

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

completedXiSurface_symmetry_only_no_go in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
pureVectorCDoublingData_offline_example in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
toyCompletedXiSurface_has_off_critical_zero in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
zeroDeviationSet_neg_closed_not_enough in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
CompletedXiSurface in IndisputableMonolith.NumberTheory.CompletedXiSymmetry decl_use
toyXi in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
toyXi_conjugation in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
toyXi_reflection in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use