`AbstractHarmonicAnalysisCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS
domain: Mathematics
line: 31 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS on GitHub at line 31.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  28def z8Size : ℕ := 8
  29theorem z8Size_2cubed : z8Size = 2 ^ 3 := by decide
  30
  31structure AbstractHarmonicAnalysisCert where
  32  five_groups : Fintype.card LCGroup = 5
  33  z8_size : z8Size = 2 ^ 3
  34
  35def abstractHarmonicAnalysisCert : AbstractHarmonicAnalysisCert where
  36  five_groups := lcGroupCount
  37  z8_size := z8Size_2cubed
  38
  39end IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.