mulETransformLeft_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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