mulLeft — Mathlib

English

Left multiplication in a Group G by a fixed element a ∈ G is a permutation of G.

Русский

Левое перенесение по фиксированному элементу a ∈ G — перестановка множества G.

LaTeX

$$$L_a: G \\to G,\\ L_a(x) = a x$ is a bijection.$$

Lean4

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

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