OAI/Probability/FreeIsing/Trees/RootedProjectivity.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.ConnectedFinset.exists_prunable_vertex_of_shared_minline 10 - theorem
OAI.Problem367.finiteFreeIsingPMF_map_subset_of_shared_minline 62 - theorem
OAI.Problem367.finiteFreeIsingPMF_map_subset_of_root_memline 93