Theorems · Theorem · combinatorics

DiscreteTiling.PlacedTile.ext_iff

∀ {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 = y ↔ x.index = y.index ∧ x.groupElts ≍ y.groupElts

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

0 results in Mathlib

Foundations

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