toPermInj

Mathlib.GroupTheory.RegularWreathProduct

URI: https://scilib.ai/kg/mathlib#RegularWreathProduct.toPermInj

English

If Λ is nonempty, then the map toPerm is injective.

Русский

Если Λ непусто, то отображение toPerm инъективно.

LaTeX

$$$ [Nonempty \Lambda] : Function.Injective (toPerm D Q Λ) $$$

Lean4

theorem toPermInj [Nonempty Λ] : Function.Injective (toPerm D Q Λ) :=
  MulAction.toPerm_injective

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

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

Разделы

Аффилиация

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