mul_left_surjective — Mathlib

English

The map x ↦ a · x from G to G is surjective for any a ∈ G when G is a group; equivalently, for every x there exists y with a · y = x, given by y = a^{-1} · x.

Русский

Отображение x ↦ a · x из группы G в себя сюръективно для любого a ∈ G; то есть для каждого x существует y с a · y = x, например y = a^{-1} · x.

LaTeX

$$$\text{Surjective}(a \cdot \_)$$$

Lean4

@[to_additive]
theorem mul_left_surjective (a : G) : Surjective (a * ·) := fun x ↦ ⟨a⁻¹ * x, mul_inv_cancel_left a x⟩

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