isSelfAdjoint_conjugate_iff_of_isUnit

English

If u is a unit, then IsSelfAdjoint (u a u*) iff IsSelfAdjoint a.

Русский

Если u — единичный элемент (обратимый), то IsSelfAdjoint(u a u*) эквивално IsSelfAdjoint a.

LaTeX

$$$\text{IsUnit}(u) \rightarrow \bigl( \text{IsSelfAdjoint}(u a u^*) \iff \text{IsSelfAdjoint}(a) \bigr)$$$

Lean4

@[grind =]
theorem _root_.isSelfAdjoint_conjugate_iff_of_isUnit {a u : R} (hu : IsUnit u) :
    IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a := by
  simp [IsSelfAdjoint, mul_assoc, hu.mul_right_inj, hu.star.mul_left_inj]

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