isSelfAdjoint_conjugate_iff_of_isUnit'

English

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

Русский

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

LaTeX

$$$\text{IsUnit}(u) \rightarrow \bigl( \text{IsSelfAdjoint}(\star u \cdot a \cdot u) \iff \text{IsSelfAdjoint}(a) \bigr)$$$

Lean4

@[grind =]
theorem _root_.isSelfAdjoint_conjugate_iff_of_isUnit' {a u : R} (hu : IsUnit u) :
    IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a := by simpa using isSelfAdjoint_conjugate_iff_of_isUnit hu.star

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