Skip to content

Commit 9855b60

Browse files
tb65536kbuzzard
andauthored
Update Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
1 parent 4e2a6b9 commit 9855b60

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ theorem IsSRGWith.ediam_eq_two [Nontrivial V] (h : G.IsSRGWith n k ℓ μ) (ht :
8383
can be reformulated as the existence of a strongly regular graph with params (99, 14, 1, 2).
8484
This is an open problem, and has no known proof of existence. -/
8585
proof_wanted conway_99 : ∃ (α : Type) (_ : Fintype α) (g : SimpleGraph α) (_ : DecidableRel g.Adj),
86-
IsSRGWith g 99 14 1 2
86+
IsSRGWith g 99 14 1 2
8787

8888
variable [DecidableEq V]
8989

0 commit comments

Comments
 (0)