seven_decomp

formal source

  46
  47theorem four_decomp : (4 : ℕ) = G2^2 := by decide
  48theorem six_decomp : (6 : ℕ) = G2 * G3 := by decide
  49theorem seven_decomp : (7 : ℕ) = G2^3 - 1 := by decide
  50theorem eight_decomp : (8 : ℕ) = G2^3 := by decide
  51theorem ten_decomp : (10 : ℕ) = G2 * G5 := by decide
  52theorem twelve_decomp : (12 : ℕ) = G2^2 * G3 := by decide
  53theorem fifteen_decomp : (15 : ℕ) = G3 * G5 := by decide
  54theorem sixteen_decomp : (16 : ℕ) = G2^4 := by decide
  55theorem twentyfive_decomp : (25 : ℕ) = G5^2 := by decide
  56theorem fortyfive_decomp : (45 : ℕ) = G3^2 * G5 := by decide
  57theorem seventy_decomp : (70 : ℕ) = Nat.choose (G2^3) (G2^2) := by decide
  58theorem oneTwentyFive_decomp : (125 : ℕ) = G5^3 := by decide
  59theorem twoSixteen_decomp : (216 : ℕ) = (G2 * G3)^3 := by decide
  60theorem twoFiftySix_decomp : (256 : ℕ) = G2^(G2^3) := by decide
  61theorem threeSixty_decomp : (360 : ℕ) = G2^3 * G3^2 * G5 := by decide
  62theorem threeOneTwentyFive_decomp : (3125 : ℕ) = G5^5 := by decide
  63
  64/-! ## Closure properties. -/
  65
  66/-- The set {2, 3, 5} is the smallest generating set for the spectrum. -/
  67theorem generators_minimal :
  68    G2 ≠ G3 ∧ G3 ≠ G5 ∧ G2 ≠ G5 := by
  69  refine ⟨?_, ?_, ?_⟩ <;> decide
  70
  71/-- The product of all three generators: 2 · 3 · 5 = 30 (= primorial p₃#). -/
  72theorem primorial_product : G2 * G3 * G5 = 30 := by decide
  73
  74/-- 30 is the third primorial. The primorial spectrum is RS-canonical:
  75    p₁# = 2, p₂# = 6, p₃# = 30, p₄# = 210. -/
  76theorem second_primorial : G2 * G3 = 6 := by decide
  77theorem third_primorial : G2 * G3 * G5 = 30 := by decide
  78
  79structure RecognitionGeneratorsCert where