isLeftInversion_inv_iff — Mathlib

English

The left inversion of w^{-1} with respect to t is equivalent to the right inversion of w with respect to t.

Русский

Левое инвертирование w^{-1} относительно t эквивалентно правому инвертированию w относительно t.

LaTeX

$$$cs.IsLeftInversion (w^{-1}) t \leftrightarrow cs.IsRightInversion w t$$$

Lean4

theorem isLeftInversion_inv_iff {w t : W} : cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t :=
  by
  convert cs.isRightInversion_inv_iff.symm
  simp

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