Theorems · Inductive type · combinatorics

DiscreteTiling.PlacedTile

{G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} → [inst : Group G] → [inst_1 : MulAction G X] → DiscreteTiling.Protoset G X ιₚ → Type (max u_1 u_3)

A PlacedTile ps is an image of a tile in the protoset p under an element of the group G. This is represented using a quotient so that images under group elements differing only by a symmetry of the tile are equal.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

18 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GroupMulAction