English
A right transversal can be viewed as a function mapping each group element to the chosen representative from its right coset.
Русский
Правый трансверсал задаёт отображение элемента группы в выбранного представителя из правого косета.
LaTeX
$$$\\text{toRightFun}(hT) : G \\to T\\;:=\\; \\text{rightQuotientEquiv}(hT)\\circ q''$$$
Lean4
/-- A right transversal can be viewed as a function mapping each element of the group
to the chosen representative from that right coset. -/
@[to_additive /-- A right transversal can be viewed as a function mapping each element of the group
to the chosen representative from that right coset. -/
]
noncomputable def toRightFun (hT : IsComplement H T) : G → T :=
rightQuotientEquiv hT ∘ .mk''
