mulRight — Mathlib

English

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

Русский

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

LaTeX

$$$R_u(x) = x u, \\; R_u \\text{ is a bijection on } M$$$

Lean4

/-- Right multiplication in a `Group` is a permutation of the underlying type. -/
@[to_additive /-- Right addition in an `AddGroup` is a permutation of the underlying type. -/
    ]
protected def mulRight (a : G) : Perm G :=
  (toUnits a).mulRight

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