coe_mulLeft

Mathlib.Algebra.Group.Units.Equiv

URI: https://scilib.ai/kg/mathlib#Equiv.coe_mulLeft

English

For a fixed group G and element a ∈ G, the map x ↦ a x is a permutation of G.

Русский

Для фиксированной группы G и элемента a ∈ G отображение x ↦ a x — перестановка G.

LaTeX

$$$f_a(x) = a x, \\quad f_a \\text{ bijective on } G$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mulLeft (a : G) : ⇑(Equiv.mulLeft a) = (a * ·) :=
  rfl

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

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

Разделы

Аффилиация

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