isLeftInversion_mul_right_iff — Mathlib

English

The left inversion of t w with respect to t is equivalent to not having a left inversion of w with respect to t.

Русский

Левое инвертирование t w относительно t эквивалентно тому, что у w нет левого инверирования относительно t.

LaTeX

$$$cs.IsLeftInversion (t \cdot w) t \leftrightarrow \neg cs.IsLeftInversion w t$$$

Lean4

theorem isLeftInversion_mul_right_iff {w : W} : cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t := by
  rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv, ht.isRightInversion_mul_left_iff]

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