def
definition
xiSensorPickRouteStatus
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.RiemannHypothesis.XiSensorPickPositivity on GitHub at line 159.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
156 schur_to_zero_free_open :
157 ∀ X : XiCayleyField, XiSchurNoPolesPrinciple X → Prop
158
159def xiSensorPickRouteStatus : XiSensorPickRouteStatus where
160 pick_to_schur := schur_of_finitePickPositive
161 schur_to_zero_free_open := fun _ _ => True
162
163end
164
165end XiSensorPickPositivity
166end RiemannHypothesis
167end NumberTheory
168end IndisputableMonolith