bijective₀ — Mathlib

English

Let G₀ be a group with zero and α a set with a G₀-action. If a ≠ 0, then the map x ↦ a • x is bijective.

Русский

Пусть G₀ - группа с нулём, α — множество с действием G₀. Если a ≠ 0, отображение x ↦ a • x биективно.

LaTeX

$$$a \neq 0 \Rightarrow \mathrm{Bijective}(x \mapsto a \cdot x)$$$

Lean4

protected theorem bijective₀ (ha : a ≠ 0) : Bijective (a • · : α → α) :=
  MulAction.bijective <| Units.mk0 a ha

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