mul_right_surjective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_right_surjective (a : G) : Function.Surjective fun x ↦ x * a := fun x ↦ ⟨x * a⁻¹, inv_mul_cancel_right x a⟩

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