feat: Self-adjoint LinearPMaps are densely defined (#6075)

Define the star on `LinearPMap` as the adjoint and prove that every self-adjoint operator is automatically densely defined.

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -243,3 +243,36 @@ theorem toPMap_adjoint_eq_adjoint_toPMap_of_dense (hp : Dense (p : Set E)) :
 #align continuous_linear_map.to_pmap_adjoint_eq_adjoint_to_pmap_of_dense ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense
 
 end ContinuousLinearMap
+
+section Star
+
+namespace LinearPMap
+
+variable [CompleteSpace E]
+
+instance instStar : Star (E →ₗ.[𝕜] E) where
+  star := fun A ↦ A.adjoint
+
+variable {A : E →ₗ.[𝕜] E}
+
+theorem isSelfAdjoint_def : IsSelfAdjoint A ↔ A† = A := Iff.rfl
+
+/-- Every self-adjoint `LinearPMap` has dense domain.
+
+This is not true by definition since we define the adjoint without the assumption that the
+domain is dense, but the choice of the junk value implies that a `LinearPMap` cannot be self-adjoint
+if it does not have dense domain. -/
+theorem _root_.IsSelfAdjoint.dense_domain (hA : IsSelfAdjoint A) : Dense (A.domain : Set E) := by
+  by_contra h
+  rw [isSelfAdjoint_def] at hA
+  have h' : A.domain = ⊤ := by
+    rw [← hA, Submodule.eq_top_iff']
+    intro x
+    rw [mem_adjoint_domain_iff, ← hA]
+    refine (innerSL 𝕜 x).cont.comp ?_
+    simp [adjoint, h, continuous_const]
+  simp [h'] at h
+
+end LinearPMap
+
+end Star