Theorems · Inductive type · combinatorics

DiscreteTiling.Prototile

(G : Type u_1) → (X : Type u_2) → [inst : Group G] → [MulAction G X] → Type (max u_1 u_2)

A Prototile G X describes a tile in X, copies of which under elements of G may be used in tilings. Two copies related by an element of symmetries are considered the same; two copies not so related, even if they have the same points, are considered distinct.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

14 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

GroupMulAction