symm_smul

Mathlib.MeasureTheory.Group.MeasurableEquiv

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

English

For every g ∈ G, the inverse of the smul automorphism equals smul by g⁻¹.

Русский

Для каждого g ∈ G обратное к аутоморфизму умножения слева совпадает со смулом g⁻¹.

LaTeX

$$$$ (\\mathrm{smul}\\, g)^{-1} = \\mathrm{smul}\\, g^{-1}. $$$$

Lean4

@[to_additive (attr := simp)]
theorem symm_smul (c : G) : (smul c : α ≃ᵐ α).symm = smul c⁻¹ :=
  ext rfl

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

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

Разделы

Аффилиация

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