102theorem IsMockOrder_iff (p : ℕ) : 103 IsMockOrder p ↔ (p = 3 ∨ p = 5 ∨ p = 7) := by
proof body
Term-mode proof.
104 constructor 105 · intro ⟨hp, hcop, hlt⟩ 106 exact mock_orders_complete p hp hcop hlt 107 · rintro (rfl | rfl | rfl) 108 · exact ⟨by decide, by decide, by omega⟩ 109 · exact ⟨by decide, by decide, by omega⟩ 110 · exact ⟨by decide, by decide, by omega⟩ 111 112/-! ## §3. Congruence Primes: Smallest Primes Coprime to 24 -/ 113 114/-- A prime is congruence-eligible if it is coprime to 24. 115 Since 24 = 2³×3, this means: the prime is neither 2 nor 3. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.