We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 01cceef commit 4e2a6b9Copy full SHA for 4e2a6b9
1 file changed
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
@@ -82,7 +82,8 @@ theorem IsSRGWith.ediam_eq_two [Nontrivial V] (h : G.IsSRGWith n k ℓ μ) (ht :
82
/-- **Conway's 99-graph problem** (from https://oeis.org/A248380/a248380.pdf)
83
can be reformulated as the existence of a strongly regular graph with params (99, 14, 1, 2).
84
This is an open problem, and has no known proof of existence. -/
85
-proof_wanted conway_99 : ∃ α : Type*, ∃ (g : SimpleGraph α), IsSRGWith G 99 14 1 2
+proof_wanted conway_99 : ∃ (α : Type) (_ : Fintype α) (g : SimpleGraph α) (_ : DecidableRel g.Adj),
86
+ IsSRGWith g 99 14 1 2
87
88
variable [DecidableEq V]
89
0 commit comments