divRight₀ — Mathlib

English

Right division by a nonzero a is a permutation with inverse x ↦ x a.

Русский

Правое деление на ненулевой a образует перестановку с обратной функцией x ↦ x a.

LaTeX

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

Lean4

/-- Right division by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! +simpRhs]
def divRight₀ (a : G₀) (ha : a ≠ 0) : Perm G₀ where
  toFun := (· / a)
  invFun := (· * a)
  left_inv _ := by simp [ha]
  right_inv _ := by simp [ha]

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