mul_left_surjective₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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