def
definition
recognitionThetaModularAttackSurface
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.RecognitionTheta.ModularIdentity on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
58 constructor :
59 RecognitionThetaPrefactor → RecognitionThetaModularIdentity
60
61def recognitionThetaModularAttackSurface :
62 RecognitionThetaModularAttackSurface where
63 prefactor_equivalence := recognitionThetaModularIdentity_iff_prefactor
64 constructor := recognitionThetaModularIdentity_of_prefactor
65
66end
67
68end ModularIdentity
69end RecognitionTheta
70end NumberTheory
71end IndisputableMonolith