image_mul_right' — Mathlib

English

Similarly, the map x → x b^{-1} is the inverse of x → x b, giving an explicit description of the image under right multiplication by b.

Русский

Аналогично отображение x → x b^{-1} является обратным к x → x b, что даёт явное описание образа при правом умножении на b.

LaTeX

$$$\operatorname{image}(x \mapsto x b^{-1})(t) = \operatorname{preimage}(t)(x \mapsto x b)$$$

Lean4

@[to_additive]
theorem image_mul_right' : image (· * b⁻¹) t = preimage t (· * b) (mul_left_injective _).injOn := by simp

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