Theorems · Theorem · combinatorics

DiscreteTiling.PlacedTile.ext

∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {ps : DiscreteTiling.Protoset G X ιₚ} {x y : DiscreteTiling.PlacedTile ps},
  x.index = y.index → x.groupElts ≍ y.groupElts → x = y

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

3 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound