Commit 2025-06-25 16:13 6116fda8
View on Github →refactor: make SimpleGraph.incMatrix computable (#25659)
This came up in a project at "Autoformalization for the Working Mathematician" at ICERM.
There are no downstream uses of this file, nor is there any implementation note explaining why noncomputable is used here; so let's make #eval work:
-- now works
#eval (⊤ : SimpleGraph (Fin 3)).incMatrix ℕ * ((⊤ : SimpleGraph (Fin 3)).incMatrix ℕ)ᵀ
This also adds some missing Matrix.ofs.