English
Describes how t^u acts on a group element g inside a normal word: the result is a pair consisting of an element from a subgroup and the coset part, given by mapping g through a certain equivalence and collecting the two parts.
Русский
Показывается разложение действия t^u на элемент g внутри нормальной формы слова: пара состоит из элемента подгруппы и компоненты косета, получаемой через заданное эквивалентное отображение.
LaTeX
$$$\\text{unitsSMulGroup}(u,g) = (a,g')$ where\\ $(a,g') = (\\operatorname{toSubgroupEquiv}\\;\\varphi\\; u\\; g'.1,\\; g'.2)$ with\\ $g' = (d^{\\mathrm{compl}}(u)).\\mathrm{equiv}(g).$$$
Lean4
/-- The action of `t^u` on `ofGroup g`. The normal form will be
`a * t^u * g'` where `a ∈ toSubgroup A B (-u)` -/
noncomputable def unitsSMulGroup (u : ℤˣ) (g : G) : (toSubgroup A B (-u)) × d.set u :=
let g' := (d.compl u).equiv g
(toSubgroupEquiv φ u g'.1, g'.2)
