isRightInversion_inv_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isRightInversion_inv_iff {w t : W} : cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t :=
  by
  apply and_congr_right
  intro ht
  rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]

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