module
module
IndisputableMonolith.Verification.WallpaperClassificationBridge
show as:
view Lean formalization →
depends on (1)
declarations in this module (13)
-
def
edge_generated_groups -
def
face_generated_groups -
theorem
W_decomposition -
theorem
W_eq_17 -
inductive
WallpaperGroup -
theorem
wallpaper_group_count -
inductive
SymmetryType -
def
dominantType -
def
edge_dominant_count -
def
face_dominant_count -
theorem
edge_dominant_eq_Ep -
theorem
face_dominant_eq_F -
theorem
total_matches_W