English
If Cancels u w holds, then we can form a new word by left-multiplying a subgroup element with g, using the subgroup equivalence, yielding a valid normal form word.
Русский
Если выполняется Cancels u w, то образуется новое слово путём левополосного умножения на элемент подгруппы и применения эквивалентности подгруппа, образующее нормальную форму.
LaTeX
$$$\\text{unitsSMulWithCancel}(u,w,\\, \\mathrm{Cancels}\\;u\\;w) := \\text{consRecOn}(w, \\ldots,\\; (\\text{toSubgroupEquiv}\\;\\varphi\\; u\\; w.head) \\; • \\; w).$$$
Lean4
/-- Multiplying `t^u` by a `NormalWord`, `w` and putting the result in normal form. -/
noncomputable def unitsSMul (u : ℤˣ) (w : NormalWord d) : NormalWord d :=
letI := Classical.dec
if h : Cancels u w then unitsSMulWithCancel φ u w h
else
let g' := unitsSMulGroup φ d u w.head
cons g'.1 u ((g'.2 * w.head⁻¹ : G) • w) (by simp)
(by
simp only [g', group_smul_toList, Option.mem_def, Option.map_eq_some_iff, Prod.exists, exists_and_right,
exists_eq_right, group_smul_head, inv_mul_cancel_right, forall_exists_index, unitsSMulGroup]
simp only [Cancels, Option.map_eq_some_iff, Prod.exists, exists_and_right, exists_eq_right, not_and,
not_exists] at h
intro u' x hx hmem
have : w.head ∈ toSubgroup A B u :=
by
have := (d.compl u).rightCosetEquivalence_equiv_snd w.head
rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this
simp_all
have := h this x
simp_all [Int.units_ne_iff_eq_neg])
