@[simp]

theorem mem_selfAdjoint_submodule_iff_isSymm {N : ℕ+} {A : Matrix (Fin ↑N) (Fin ↑N) ℝ} : A ∈ selfAdjoint.submodule ℝ (Matrix (Fin ↑N) (Fin ↑N) ℝ) ↔ A.IsSymm

Example 2.5: for a strictly positive integer N, the real vector subspace of symmetric N × N matrices is the canonical self-adjoint submodule of Matrix (Fin N) (Fin N) ℝ; equivalently, membership is the library predicate A.IsSymm.

theorem mem_selfAdjoint_submodule_iff {N : ℕ+} {A : Matrix (Fin ↑N) (Fin ↑N) ℝ} : A ∈ selfAdjoint.submodule ℝ (Matrix (Fin ↑N) (Fin ↑N) ℝ) ↔ A.transpose = A

Example 2.5 in textbook coordinates: membership in the canonical self-adjoint submodule is the condition Aᵀ = A.