Theorems · Definition · combinatorics

DiscreteTiling.Prototile.symmetries

{G : Type u_1} →
  {X : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] → (self : DiscreteTiling.Prototile G X) → Subgroup ↥(MulAction.stabilizer G ↑self)

The group elements considered to be symmetries of the prototile.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

18 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

GroupMulAction