symm_mulRight

Mathlib.MeasureTheory.Group.MeasurableEquiv

URI: https://scilib.ai/kg/mathlib#MeasurableEquiv.symm_mulRight

English

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

Русский

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

LaTeX

$$$(\\mathrm{mulRight}(g))^{-1} = \\mathrm{mulRight}(g^{-1})$$$

Lean4

@[to_additive (attr := simp)]
theorem symm_mulRight (g : G) : (mulRight g).symm = mulRight g⁻¹ :=
  ext rfl

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

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

Разделы

Аффилиация

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