viaEmbeddingHom — Mathlib

English

viaEmbeddingHom is a group homomorphism sending a permutation on α to its extended-domain permutation on β.

Русский

viaEmbeddingHom — гомоморфизм группы, переводящий перестановку на α в перестановку на β через расширение области определения.

LaTeX

$$viaEmbeddingHom : Perm(α) →* Perm(β)$$

Lean4

/-- `viaEmbedding` as a group homomorphism -/
noncomputable def viaEmbeddingHom : Perm α →* Perm β :=
  extendDomainHom (ofInjective ι.1 ι.2)

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