module module

`IndisputableMonolith.CrossDomain.RecognitionGenerators`

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 (25)

def G2 L41
def G3 L42
def G5 L43
theorem four_decomp L47
theorem six_decomp L48
theorem seven_decomp L49
theorem eight_decomp L50
theorem ten_decomp L51
theorem twelve_decomp L52
theorem fifteen_decomp L53
theorem sixteen_decomp L54
theorem twentyfive_decomp L55
theorem fortyfive_decomp L56
theorem seventy_decomp L57
theorem oneTwentyFive_decomp L58
theorem twoSixteen_decomp L59
theorem twoFiftySix_decomp L60
theorem threeSixty_decomp L61
theorem threeOneTwentyFive_decomp L62
theorem generators_minimal L67
theorem primorial_product L72
theorem second_primorial L76
theorem third_primorial L77
structure RecognitionGeneratorsCert L79
def recognitionGeneratorsCert L92