Theorems · Theorem · dynamical systems

SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_mem

∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : Monoid G] [IsLeftCancelMul G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (v w : G), w ∈ p.support → p.mulShift v (v * w) = p.config w

On the translated support, p.mulShift v agrees with p.config at the preimage. More precisely, if w ∈ p.support, then at the translated site v * w, the configuration p.mulShift v takes the value p.config w. This uses [IsLeftCancelMul G] to identify the unique preimage of v * w under left-multiplication by v.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

InhabitedMonoidIsLeftCancelMul