class IsMaximalSelfAdjoint (R : outParam (Type u_1)) (α : Type u_2) [Star α] [Star R] [CommSemiring R] [Semiring α] [TrivialStar R] [Algebra R α] : Type (max u_1 u_2)

• selfadjMap : α →+ R
• selfadj_smul (r : R) (a : α) : selfadjMap (r • a) = r * selfadjMap a
• selfadj_algebra {a : α} : IsSelfAdjoint a → (algebraMap R α) (selfadjMap a) = a

instance instTrivialStar_IsMaximalSelfAdjoint {R : Type u_1} [Star R] [TrivialStar R] [CommSemiring R] : IsMaximalSelfAdjoint R R

Every TrivialStar CommSemiring is its own maximal self adjoints.

Equations

• instTrivialStar_IsMaximalSelfAdjoint = { selfadjMap := AddMonoidHom.id R, selfadj_smul := ⋯, selfadj_algebra := ⋯ }

instance instRCLike_IsMaximalSelfAdjoint {α : Type u_1} [RCLike α] : IsMaximalSelfAdjoint ℝ α

ℝ is the maximal self adjoint elements over RCLike

Equations

• instRCLike_IsMaximalSelfAdjoint = { selfadjMap := RCLike.re, selfadj_smul := ⋯, selfadj_algebra := ⋯ }

@[simp]

theorem IsMaximalSelfAdjoint.trivial_selfadjMap {R : Type u_1} [Star R] [TrivialStar R] [CommSemiring R] : selfadjMap = AddMonoidHom.id R

@[simp]

theorem IsMaximalSelfAdjoint.RCLike_selfadjMap {α : Type u_1} [RCLike α] : selfadjMap = RCLike.re