mulRight — Mathlib

English

Right multiplication by a unit u ∈ Mˣ is a permutation of the underlying type.

Русский

Правое умножение на единицу u ∈ Mˣ образует перестановку основывая тип.

LaTeX

$$$\\text{Let } g(x) = x u. \\; g \\text{ is a bijection on } M.$$$

Lean4

/-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
@[to_additive (attr := simps -fullyApplied apply) /--
    Right addition of an additive unit is a permutation of the underlying type. -/
    ]
def mulRight (u : Mˣ) : Equiv.Perm M where
  toFun x := x * u
  invFun x := x * ↑u⁻¹
  left_inv x := mul_inv_cancel_right x u
  right_inv x := inv_mul_cancel_right x u

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