extendDomainHom — Mathlib

English

Define extendDomainHom as a monoid homomorphism from the permutation group of α to the permutation group of β, given by e ↦ extendDomain e f.

Русский

Определим extendDomainHom как гомоморфизм по умножению от группы перестановок α в перестановки β, заданный отображением e ↦ extendDomain e f.

LaTeX

$$$\mathrm{extendDomainHom}: \operatorname{Perm}(\alpha) \to^* \operatorname{Perm}(\beta) \text{ defined by } e \mapsto \operatorname{extendDomain}(e,f)$$$

Lean4

/-- `extendDomain` as a group homomorphism -/
@[simps]
def extendDomainHom : Perm α →* Perm β where
  toFun e := extendDomain e f
  map_one' := extendDomain_one f
  map_mul' e e' := (extendDomain_mul f e e').symm

Похожие утверждения