preimage_mul_left_singleton — Mathlib

English

In a group, the preimage of a singleton {b} under the map x → a x is the singleton {a^{-1} b}.

Русский

В группе предобраз множества {b} под отображением x → a x равен одиночке {a^{-1} b}.

LaTeX

$$$\operatorname{preimage} \{b\} (a \cdot \cdot) (\text{injOn}) = \{a^{-1} b\}$$$

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_left_singleton : preimage { b } (a * ·) (mul_right_injective _).injOn = {a⁻¹ * b} := by
  classical rw [← image_mul_left', image_singleton]

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