image_mul_right' — Mathlib

English

The primed version of right multiplication yields a similar equality with preimage under right multiplication by b.

Русский

Примарная версия правого умножения даёт аналогичное равенство с предобразом от правого умножения на b.

LaTeX

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

Lean4

@[to_additive]
theorem image_mul_right' : (· * b⁻¹) '' t = (· * b) ⁻¹' t := by simp

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