mulRight₀ — Mathlib

English

Right division by a nonzero element a is a permutation of G₀.

Русский

Правое деление на ненулевой элемент a является перестановкой G₀.

LaTeX

$$$a \\neq 0 \\Rightarrow \\text{Perm } (x \\mapsto x / a)$$$

Lean4

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

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