pith. machine review for the scientific record. sign in
def definition def or abbrev

recognitionThetaModularAttackSurface

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  61def recognitionThetaModularAttackSurface :
  62    RecognitionThetaModularAttackSurface where
  63  prefactor_equivalence := recognitionThetaModularIdentity_iff_prefactor

proof body

Definition body.

  64  constructor := recognitionThetaModularIdentity_of_prefactor
  65
  66end
  67
  68end ModularIdentity
  69end RecognitionTheta
  70end NumberTheory
  71end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.