English
sumCongrHom is a MonoidHom from Perm α × Perm β to Perm (α ⊕ β), with toFun(e,f) = sumCongr e f and preserving identity and multiplication.
Русский
sumCongrHom есть однородный отображение (моноид-гомоморфизм) от Perm α × Perm β к Perm(α ⊕ β), задающее toFun(e,f) = sumCongr e f и сохраняющее тождество и умножение.
LaTeX
$$$\\mathrm{sumCongrHom} : \\mathrm{Perm}(\\alpha) \\times \\mathrm{Perm}(\\beta) \\to^* \\mathrm{Perm}(\\alpha \\oplus \\beta),\\quad \\operatorname{toFun}(e,f) = \\mathrm{sumCongr}(e,f).$$$
Lean4
/-- `Equiv.Perm.sumCongr` as a `MonoidHom`, with its two arguments bundled into a single `Prod`.
This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of
permutations which do not exchange elements between `α` and `β`. -/
@[simps]
def sumCongrHom (α β : Type*) : Perm α × Perm β →* Perm (α ⊕ β)
where
toFun a := sumCongr a.1 a.2
map_one' := sumCongr_one
map_mul' _ _ := (sumCongr_mul _ _ _ _).symm
