viaEmbeddingHom_apply

Mathlib.GroupTheory.Perm.ViaEmbedding

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.viaEmbeddingHom_apply

English

The monoid-homomorphism viaEmbeddingHom agrees with the explicit viaEmbedding construction.

Русский

Гомоморфизм viaEmbeddingHom согласуется с явной конструкцией viaEmbedding.

LaTeX

$$(viaEmbeddingHom ι)(e) = viaEmbedding e ι$$

Lean4

theorem viaEmbeddingHom_apply : viaEmbeddingHom ι e = viaEmbedding e ι :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru