mul_right_surjective₀ — Mathlib

English

If a ≠ 0, then right multiplication by a is surjective: for any target, there exists g with g · a equal to it.

Русский

Если a ≠ 0, то правое умножение на a является сюръективным: для любого целевого значения найдётся g с g·a = целевое.

LaTeX

$$$a \\\\neq 0 \\\\rightarrow \\\\text{Surjective}(g \\\\mapsto g \\\\cdot a)$$$

Lean4

theorem mul_right_surjective₀ {a : G₀} (h : a ≠ 0) : Surjective fun g => g * a := fun g =>
  ⟨g * a⁻¹, by simp [mul_assoc, inv_mul_cancel₀ h]⟩

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