English
Cancels(u,w) is the predicate expressing whether t^u cancels with some occurrence of t^-u when multiplying t^u by w: equivalently, membership of head in a certain subgroup together with a specific condition on the first head element.
Русский
Cancels(u,w) определяет, происходит ли отмена t^u с каким-либо t^-u внутри произведения t^u w: равносильно членству головы в подгруппе и определённому условию на первый элемент головы.
LaTeX
$$$\\mathrm{Cancels}(u,w) := (w.head \\in (toSubgroup A B \\; u)) \\wedge (w.toList.head?.map Prod.fst = \\mathrm{some}(-u)).$$$
Lean4
/-- `Cancels u w` is a predicate expressing whether `t^u` cancels with some occurrence
of `t^-u` when we multiply `t^u` by `w`. -/
def Cancels (u : ℤˣ) (w : NormalWord d) : Prop :=
(w.head ∈ (toSubgroup A B u : Subgroup G)) ∧ w.toList.head?.map Prod.fst = some (-u)
