mulRight_symm_apply — Mathlib

English

The action of the right multiplication equivalence on G is the map x ↦ x a.

Русский

Действие эквивалентности правого умножения на G задаёт отображение x ↦ x a.

LaTeX

$$$\\mathrm{Equiv.mulRight}\ (a): G \\to G,\\; x \\mapsto x a$$$

Lean4

/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
@[to_additive (attr := simp) /-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
    ]
theorem mulRight_symm_apply (a : G) : ((Equiv.mulRight a).symm : G → G) = fun x => x * a⁻¹ :=
  rfl

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