isReflection_conj_iff — Mathlib

English

If t is a reflection, then for any w, the element w t w^{-1} is a reflection.

Русский

Если t — отражение, то для любого w элемент w t w^{-1} является отражением.

LaTeX

$$$cs.IsReflection\, t \rightarrow \forall w:\, W, cs.IsReflection (w t w^{-1})$$$

Lean4

@[simp]
theorem isReflection_conj_iff (w t : W) : cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t :=
  by
  constructor
  · intro h
    simpa [← mul_assoc] using h.conj w⁻¹
  · exact IsReflection.conj (w := w)

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