divLeft₀ — Mathlib

English

Left division by a nonzero a is a permutation of G₀.

Русский

Левое деление на ненулевой a образует перестановку G₀.

LaTeX

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

Lean4

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

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