Theorems · Theorem · combinatorics

DiscreteTiling.Protoset.mk.inj

∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {tiles tiles_1 : ιₚ → DiscreteTiling.Prototile G X}, { tiles := tiles } = { tiles := tiles_1 } → tiles = tiles_1

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms