coe_mulRight

Mathlib.Algebra.Group.Units.Equiv

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

English

The inverse of the right-translation by a is right-translation by a^{-1}.

Русский

Обратное правому переносу по a — перенос по a^{-1}.

LaTeX

$$$(R_a)^{-1} = R_{a^{-1}}$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mulRight (a : G) : ⇑(Equiv.mulRight a) = fun x => x * a :=
  rfl

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

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

Разделы

Аффилиация

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