image_mul_left' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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