injective

Mathlib.Algebra.Group.Action.Basic

URI: https://scilib.ai/kg/mathlib#MulAction.injective

English

For a fixed g ∈ α, the map x ↦ g • x is injective.

Русский

Для фиксированного g ∈ α отображение x ↦ g • x инъективно.

LaTeX

$$$ \text{injective } (g \cdot -) : β \to β $$$

Lean4

@[to_additive]
protected theorem injective (g : α) : Function.Injective (g • · : β → β) :=
  (MulAction.bijective g).injective

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

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

Разделы

Аффилиация

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