`recognitionGeneratorsCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.RecognitionGenerators
domain: CrossDomain
line: 92 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.RecognitionGenerators on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  89  oneTwentyFive_as_G : (125 : ℕ) = G5^3
  90  threeSixty_as_G : (360 : ℕ) = G2^3 * G3^2 * G5
  91
  92def recognitionGeneratorsCert : RecognitionGeneratorsCert where
  93  generator_2 := rfl
  94  generator_3 := rfl
  95  generator_5 := rfl
  96  primorial_3 := primorial_product
  97  generators_distinct := generators_minimal
  98  four_as_G := four_decomp
  99  six_as_G := six_decomp
 100  fortyfive_as_G := fortyfive_decomp
 101  oneTwentyFive_as_G := oneTwentyFive_decomp
 102  threeSixty_as_G := threeSixty_decomp
 103
 104end IndisputableMonolith.CrossDomain.RecognitionGenerators

papers checked against this theorem

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