mulETransformRight_inv — Mathlib

English

The right transform with inverse e^{-1} equals the swapped left transform with swap on the input, i.e., mulETransformRight(e^{-1}, x) equals (mulETransformLeft(e, x.swap)).swap.

Русский

Правое преобразование с инверсией e^{-1} равно левому преобразованию после перестановки входа, т. е. mulETransformRight(e^{-1}, x) = (mulETransformLeft(e, x.swap)).swap.

LaTeX

$$$ \\mathrm{mulETransformRight}(e^{-1}, x) = (\\mathrm{mulETransformLeft}(e, x^{\\mathrm{swap}})).\\mathrm{swap} $$$

Lean4

@[to_additive (attr := simp)]
theorem mulETransformRight_inv : mulETransformRight e⁻¹ x = (mulETransformLeft e x.swap).swap := by
  simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]

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