Skip to content

Commit c5ed95e

Browse files
committed
exclude the "@[no_expose]" addition from this PR
1 parent 34634d7 commit c5ed95e

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/Combinatorics/SimpleGraph/Copy.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -477,7 +477,7 @@ variable [Fintype V] [Fintype W]
477477

478478
/-- `G.labeledCopyCount H` is the number of labeled copies of `H` in `G`, i.e. the number of graph
479479
embeddings from `H` to `G`. See `SimpleGraph.copyCount` for the number of unlabeled copies. -/
480-
@[no_expose] noncomputable def labeledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
480+
noncomputable def labeledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
481481
classical exact Fintype.card (Copy H G)
482482

483483
@[deprecated (since := "2026-04-30")] alias labelledCopyCount := labeledCopyCount
@@ -507,7 +507,7 @@ variable [Fintype V]
507507

508508
/-- `G.copyCount H` is the number of unlabeled copies of `H` in `G`, i.e. the number of subgraphs
509509
of `G` isomorphic to `H`. See `SimpleGraph.labeledCopyCount` for the number of labeled copies. -/
510-
@[no_expose] noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
510+
noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
511511
classical exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
512512

513513
lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : H →g G // Injective f}]

0 commit comments

Comments
 (0)