module module

`IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS`

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

declarations in this module (6)

inductive LCGroup L21
theorem lcGroupCount L25
def z8Size L28
theorem z8Size_2cubed L29
structure AbstractHarmonicAnalysisCert L31
def abstractHarmonicAnalysisCert L35