star_apply_of_isSelfAdjoint — Mathlib

English

If f is self-adjoint, then the entries satisfy star(f_{i j}) = f_{j i} via star_apply.

Русский

Если f самоприводимая, то элементы удовлетворяют star(f_{i j}) = f_{j i} через star_apply.

LaTeX

$$$[Star A] {f : CStarMatrix n n A} (hf : IsSelfAdjoint f) {i j} : \star (f_{i j}) = f_{j i}$$$

Lean4

theorem star_apply_of_isSelfAdjoint [Star A] {f : CStarMatrix n n A} (hf : IsSelfAdjoint f) {i j : n} :
    star (f i j) = f j i := by rw [← star_apply, IsSelfAdjoint.star_eq hf]

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