mulLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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