mulLeft₀ — Mathlib

English

For every nonzero a in G₀, left multiplication by a, x ↦ a x, is a permutation of the underlying set.

Русский

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

LaTeX

$$$a \\neq 0 \\Rightarrow \\{ x \\mapsto a x \\} \\text{ is bijective on } G_0$$$

Lean4

/-- Left multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! -fullyApplied]
protected def mulLeft₀ (a : G₀) (ha : a ≠ 0) : Perm G₀ :=
  (Units.mk0 a ha).mulLeft

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