pith. machine review for the scientific record. sign in
def definition def or abbrev

orbitCount

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  81def orbitCount : WallpaperGroup → ℕ
  82  | .p1 => 1
  83  | .p2 => 2
  84  | .pm => 2
  85  | .pg => 2
  86  | .cm => 2
  87  | .pmm => 4
  88  | .pmg => 4
  89  | .pgg => 4
  90  | .cmm => 4
  91  | .p4 => 4
  92  | .p4m => 8
  93  | .p4g => 8
  94  | .p3 => 3
  95  | .p3m1 => 6
  96  | .p31m => 6
  97  | .p6 => 6
  98  | .p6m => 12
  99
 100/-- The maximum-symmetry group is `p6m` with twelve canonical orbits. -/

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.