theorem
IsSelfAdjoint.conj_eq
{α : Type u_1}
[CommSemiring α]
[StarRing α]
{a : α}
(ha : IsSelfAdjoint a)
:
↑(starRingEnd α) a = a
theorem
Pi.isSelfAdjoint
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Star (α i)]
{f : (i : ι) → α i}
:
IsSelfAdjoint f ↔ ∀ (i : ι), IsSelfAdjoint (f i)
theorem
IsSelfAdjoint.apply
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Star (α i)]
{f : (i : ι) → α i}
:
IsSelfAdjoint f → ∀ (i : ι), IsSelfAdjoint (f i)
Alias of the forward direction of Pi.isSelfAdjoint.