preimage_mul_left_singleton — Mathlib

English

The preimage of a singleton under left multiplication by a is the singleton of a^{-1} b when applied to b.

Русский

Предобраз единичного множества под левым умножением на a есть единичное множество a^{-1} b для некоторого b.

LaTeX

$$$ (a \cdot \cdot)^{-1}' { b } = { a^{-1} \cdot b } $$$

Lean4

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

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