mulETransformRight_one — Mathlib

English

The right energy transform by the identity element acts trivially: for any pair x, mulETransformRight(1, x) equals x.

Русский

Правое преобразование энергии на единичном элементе действует тривиально: для любой пары x выполняется mulETransformRight(1, x) = x.

LaTeX

$$$ (\\mathrm{mulETransformRight}(1,x)) = x $$$

Lean4

@[to_additive (attr := simp)]
theorem mulETransformRight_one : mulETransformRight 1 x = x := by simp [mulETransformRight]

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