Self-adjoint, skew-adjoint and normal elements of a star additive group

This file defines selfAdjoint R (resp. skewAdjoint R), where R is a star additive group, as the additive subgroup containing the elements that satisfy star x = x (resp. star x = -x). This includes, for instance, (skew-)Hermitian operators on Hilbert spaces.

We also define IsStarNormal R, a Prop that states that an element x satisfies star x * x = x * star x.

Implementation notes

• When R is a StarModule R₂ R, then selfAdjoint R has a natural Module (selfAdjoint R₂) (selfAdjoint R) structure. However, doing this literally would be undesirable since in the main case of interest (R₂ = ℂ) we want Module ℝ (selfAdjoint R) and not Module (selfAdjoint ℂ) (selfAdjoint R). We solve this issue by adding the typeclass [TrivialStar R₃], of which ℝ is an instance (registered in Data/Real/Basic), and then add a [Module R₃ (selfAdjoint R)] instance whenever we have [Module R₃ R] [TrivialStar R₃]. (Another approach would have been to define [StarInvariantScalars R₃ R] to express the fact that star (x • v) = x • star v, but this typeclass would have the disadvantage of taking two type arguments.)

TODO

• Define IsSkewAdjoint to match IsSelfAdjoint.
• Define fun z x => z * x * star z (i.e. conjugation by z) as a monoid action of R on R (similar to the existing ConjAct for groups), and then state the fact that selfAdjoint R is invariant under it.

def IsSelfAdjoint {R : Type u_1} [Star R] (x : R) : Prop

An element is self-adjoint if it is equal to its star.

class IsStarNormal {R : Type u_1} [Mul R] [Star R] (x : R) : Prop

An element of a star monoid is normal if it commutes with its adjoint.

• star_comm_self : Commute (star x) x

  A normal element of a star monoid commutes with its adjoint.

theorem isStarNormal_iff {R : Type u_1} [Mul R] [Star R] (x : R) : IsStarNormal x ↔ Commute (star x) x

theorem star_comm_self' {R : Type u_1} [Mul R] [Star R] (x : R) [IsStarNormal x] : star x * x = x * star x

theorem IsSelfAdjoint.all {R : Type u_1} [Star R] [TrivialStar R] (r : R) : IsSelfAdjoint r

All elements are self-adjoint when star is trivial.

theorem IsSelfAdjoint.star_eq {R : Type u_1} [Star R] {x : R} (hx : IsSelfAdjoint x) : star x = x

theorem isSelfAdjoint_iff {R : Type u_1} [Star R] {x : R} : IsSelfAdjoint x ↔ star x = x

@[simp]

theorem IsSelfAdjoint.star_iff {R : Type u_1} [InvolutiveStar R] {x : R} : IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

@[simp]

theorem IsSelfAdjoint.star_mul_self {R : Type u_1} [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (star x * x)

@[simp]

theorem IsSelfAdjoint.mul_star_self {R : Type u_1} [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (x * star x)

theorem IsSelfAdjoint.commute_iff {R : Type u_3} [Mul R] [StarMul R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : Commute x y ↔ IsSelfAdjoint (x * y)

Self-adjoint elements commute if and only if their product is self-adjoint.

theorem IsSelfAdjoint.map {F : Type u_3} {R : Type u_4} {S : Type u_5} [Star R] [Star S] [FunLike F R S] [StarHomClass F R S] {x : R} (hx : IsSelfAdjoint x) (f : F) : IsSelfAdjoint (f x)

Functions in a StarHomClass preserve self-adjoint elements.

theorem isSelfAdjoint_map {F : Type u_3} {R : Type u_4} {S : Type u_5} [Star R] [Star S] [FunLike F R S] [StarHomClass F R S] [TrivialStar R] (f : F) (x : R) : IsSelfAdjoint (f x)

theorem IsSelfAdjoint.isStarNormal {R : Type u_3} [Mul R] [Star R] {x : R} (hx : IsSelfAdjoint x) : IsStarNormal x

@[simp]

theorem IsSelfAdjoint.zero (R : Type u_1) [AddMonoid R] [StarAddMonoid R] : IsSelfAdjoint 0

theorem IsSelfAdjoint.add {R : Type u_1} [AddMonoid R] [StarAddMonoid R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x + y)

theorem IsSelfAdjoint.neg {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint (-x)

theorem IsSelfAdjoint.sub {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x - y)

@[simp]

theorem IsSelfAdjoint.add_star_self {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] (x : R) : IsSelfAdjoint (x + star x)

@[simp]

theorem IsSelfAdjoint.star_add_self {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] (x : R) : IsSelfAdjoint (star x + x)

theorem IsSelfAdjoint.conjugate {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (z : R) : IsSelfAdjoint (z * x * star z)

theorem IsSelfAdjoint.conjugate' {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (z : R) : IsSelfAdjoint (star z * x * z)

theorem IsSelfAdjoint.conjugate_self {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) {z : R} (hz : IsSelfAdjoint z) : IsSelfAdjoint (z * x * z)

@[simp]

theorem IsSelfAdjoint.one (R : Type u_1) [MulOneClass R] [StarMul R] : IsSelfAdjoint 1

theorem IsSelfAdjoint.pow {R : Type u_1} [Monoid R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ℕ) : IsSelfAdjoint (x ^ n)

@[simp]

theorem IsSelfAdjoint.invOf_iff {R : Type u_1} [Monoid R] [StarMul R] (x : R) [Invertible x] : IsSelfAdjoint ⅟x ↔ IsSelfAdjoint x

theorem IsSelfAdjoint.invOf {R : Type u_1} [Monoid R] [StarMul R] (x : R) [Invertible x] : IsSelfAdjoint x → IsSelfAdjoint ⅟x

Alias of the reverse direction of IsSelfAdjoint.invOf_iff.

theorem IsUnit.isSelfAdjoint_conjugate_iff {R : Type u_1} [Monoid R] [StarMul R] {a u : R} (hu : IsUnit u) : IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a

theorem IsUnit.isSelfAdjoint_conjugate_iff' {R : Type u_1} [Monoid R] [StarMul R] {a u : R} (hu : IsUnit u) : IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

@[deprecated IsUnit.isSelfAdjoint_conjugate_iff (since := "2025-09-28")]

theorem isSelfAdjoint_conjugate_iff_of_isUnit {R : Type u_1} [Monoid R] [StarMul R] {a u : R} (hu : IsUnit u) : IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a

Alias of IsUnit.isSelfAdjoint_conjugate_iff.

@[deprecated IsUnit.isSelfAdjoint_conjugate_iff' (since := "2025-09-28")]

theorem isSelfAdjoint_conjugate_iff_of_isUnit' {R : Type u_1} [Monoid R] [StarMul R] {a u : R} (hu : IsUnit u) : IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

Alias of IsUnit.isSelfAdjoint_conjugate_iff'.

@[simp]

theorem IsSelfAdjoint.natCast {R : Type u_1} [NonAssocSemiring R] [StarRing R] (n : ℕ) : IsSelfAdjoint ↑n

@[simp]

theorem IsSelfAdjoint.ofNat {R : Type u_1} [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] : IsSelfAdjoint (OfNat.ofNat n)

theorem IsSelfAdjoint.mul {R : Type u_1} [CommSemigroup R] [StarMul R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x * y)

theorem IsSelfAdjoint.conj_eq {α : Type u_3} [CommSemiring α] [StarRing α] {a : α} (ha : IsSelfAdjoint a) : (starRingEnd α) a = a

@[simp]

theorem IsSelfAdjoint.intCast {R : Type u_1} [Ring R] [StarRing R] (z : ℤ) : IsSelfAdjoint ↑z

theorem IsSelfAdjoint.inv {R : Type u_1} [Group R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint x⁻¹

@[simp]

theorem IsSelfAdjoint.inv_iff {R : Type u_1} [Group R] [StarMul R] (x : R) : IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

theorem IsSelfAdjoint.zpow {R : Type u_1} [Group R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ℤ) : IsSelfAdjoint (x ^ n)

theorem IsSelfAdjoint.inv₀ {R : Type u_1} [GroupWithZero R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint x⁻¹

@[simp]

theorem IsSelfAdjoint.inv₀_iff {R : Type u_1} [GroupWithZero R] [StarMul R] (x : R) : IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

theorem IsSelfAdjoint.zpow₀ {R : Type u_1} [GroupWithZero R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ℤ) : IsSelfAdjoint (x ^ n)

@[simp]

theorem IsSelfAdjoint.nnratCast {R : Type u_1} [DivisionSemiring R] [StarRing R] (q : ℚ≥0) : IsSelfAdjoint ↑q

@[simp]

theorem IsSelfAdjoint.ratCast {R : Type u_1} [DivisionRing R] [StarRing R] (x : ℚ) : IsSelfAdjoint ↑x

theorem IsSelfAdjoint.div {R : Type u_1} [Semifield R] [StarRing R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y)

theorem IsSelfAdjoint.smul {R : Type u_1} {A : Type u_2} [Star R] [Star A] [SMul R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) {x : A} (hx : IsSelfAdjoint x) : IsSelfAdjoint (r • x)

theorem IsSelfAdjoint.smul_iff {R : Type u_1} {A : Type u_2} [Monoid R] [StarMul R] [Star A] [MulAction R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) (hu : IsUnit r) {x : A} : IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

def selfAdjoint (R : Type u_1) [AddGroup R] [StarAddMonoid R] : AddSubgroup R

The self-adjoint elements of a star additive group, as an additive subgroup.

def skewAdjoint (R : Type u_1) [AddCommGroup R] [StarAddMonoid R] : AddSubgroup R

The skew-adjoint elements of a star additive group, as an additive subgroup.

theorem selfAdjoint.mem_iff {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} : x ∈ selfAdjoint R ↔ star x = x

@[simp]

theorem selfAdjoint.star_val_eq {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : ↥(selfAdjoint R)} : star ↑x = ↑x

@[implicit_reducible]

instance selfAdjoint.instInhabitedSubtypeMemAddSubgroup {R : Type u_1} [AddGroup R] [StarAddMonoid R] : Inhabited ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.isSelfAdjoint {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : ↥(selfAdjoint R)} : IsSelfAdjoint ↑x

instance selfAdjoint.isStarNormal {R : Type u_1} [NonUnitalRing R] [StarRing R] (x : ↥(selfAdjoint R)) : IsStarNormal ↑x

@[implicit_reducible]

instance selfAdjoint.instOneSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] : One ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [StarRing R] : ↑1 = 1

instance selfAdjoint.instNontrivialSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] [Nontrivial R] : Nontrivial ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instNatCastSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] : NatCast ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instIntCastSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] : IntCast ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instPowSubtypeMemAddSubgroupNat {R : Type u_1} [Ring R] [StarRing R] : Pow ↥(selfAdjoint R) ℕ

@[simp]

theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [StarRing R] (x : ↥(selfAdjoint R)) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[implicit_reducible]

instance selfAdjoint.instMulSubtypeMemAddSubgroup {R : Type u_1} [NonUnitalCommRing R] [StarRing R] : Mul ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.val_mul {R : Type u_1} [NonUnitalCommRing R] [StarRing R] (x y : ↥(selfAdjoint R)) : ↑(x * y) = ↑x * ↑y

@[implicit_reducible]

instance selfAdjoint.instCommRingSubtypeMemAddSubgroup {R : Type u_1} [CommRing R] [StarRing R] : CommRing ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instInvSubtypeMemAddSubgroup {R : Type u_1} [Field R] [StarRing R] : Inv ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.val_inv {R : Type u_1} [Field R] [StarRing R] (x : ↥(selfAdjoint R)) : ↑x⁻¹ = (↑x)⁻¹

@[implicit_reducible]

instance selfAdjoint.instDivSubtypeMemAddSubgroup {R : Type u_1} [Field R] [StarRing R] : Div ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.val_div {R : Type u_1} [Field R] [StarRing R] (x y : ↥(selfAdjoint R)) : ↑(x / y) = ↑x / ↑y

@[implicit_reducible]

instance selfAdjoint.instPowSubtypeMemAddSubgroupInt {R : Type u_1} [Field R] [StarRing R] : Pow ↥(selfAdjoint R) ℤ

@[simp]

theorem selfAdjoint.val_zpow {R : Type u_1} [Field R] [StarRing R] (x : ↥(selfAdjoint R)) (z : ℤ) : ↑(x ^ z) = ↑x ^ z

@[implicit_reducible]

instance selfAdjoint.instNNRatCast {R : Type u_1} [Field R] [StarRing R] : NNRatCast ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instRatCast {R : Type u_1} [Field R] [StarRing R] : RatCast ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.val_nnratCast {R : Type u_1} [Field R] [StarRing R] (q : ℚ≥0) : ↑↑q = ↑q

@[simp]

theorem selfAdjoint.val_ratCast {R : Type u_1} [Field R] [StarRing R] (q : ℚ) : ↑↑q = ↑q

@[implicit_reducible]

instance selfAdjoint.instSMulNNRat {R : Type u_1} [Field R] [StarRing R] : SMul ℚ≥0 ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instSMulRat {R : Type u_1} [Field R] [StarRing R] : SMul ℚ ↥(selfAdjoint R)

@[simp]

theorem selfAdjoint.val_nnqsmul {R : Type u_1} [Field R] [StarRing R] (q : ℚ≥0) (x : ↥(selfAdjoint R)) : ↑(q • x) = q • ↑x

@[simp]

theorem selfAdjoint.val_qsmul {R : Type u_1} [Field R] [StarRing R] (q : ℚ) (x : ↥(selfAdjoint R)) : ↑(q • x) = q • ↑x

@[implicit_reducible]

instance selfAdjoint.instField {R : Type u_1} [Field R] [StarRing R] : Field ↥(selfAdjoint R)

@[implicit_reducible]

instance selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [SMul R A] [StarModule R A] : SMul R ↥(selfAdjoint A)

@[simp]

theorem selfAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [SMul R A] [StarModule R A] (r : R) (x : ↥(selfAdjoint A)) : ↑(r • x) = r • ↑x

@[implicit_reducible]

instance selfAdjoint.instMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [Monoid R] [MulAction R A] [StarModule R A] : MulAction R ↥(selfAdjoint A)

@[implicit_reducible]

instance selfAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] : DistribMulAction R ↥(selfAdjoint A)

@[implicit_reducible]

instance selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Semiring R] [Module R A] [StarModule R A] : Module R ↥(selfAdjoint A)

theorem skewAdjoint.mem_iff {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : R} : x ∈ skewAdjoint R ↔ star x = -x

@[simp]

theorem skewAdjoint.star_val_eq {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : ↥(skewAdjoint R)} : star ↑x = -↑x

@[implicit_reducible]

instance skewAdjoint.instInhabitedSubtypeMemAddSubgroup {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] : Inhabited ↥(skewAdjoint R)

theorem skewAdjoint.conjugate {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x ∈ skewAdjoint R) (z : R) : z * x * star z ∈ skewAdjoint R

theorem skewAdjoint.conjugate' {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x ∈ skewAdjoint R) (z : R) : star z * x * z ∈ skewAdjoint R

theorem skewAdjoint.isStarNormal_of_mem {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x ∈ skewAdjoint R) : IsStarNormal x

instance skewAdjoint.instIsStarNormalValMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] (x : ↥(skewAdjoint R)) : IsStarNormal ↑x

theorem skewAdjoint.smul_mem {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A} (h : x ∈ skewAdjoint A) : r • x ∈ skewAdjoint A

@[implicit_reducible]

instance skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] : SMul R ↥(skewAdjoint A)

@[simp]

theorem skewAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) (x : ↥(skewAdjoint A)) : ↑(r • x) = r • ↑x

@[implicit_reducible]

instance skewAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] : DistribMulAction R ↥(skewAdjoint A)

@[implicit_reducible]

instance skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Semiring R] [Module R A] [StarModule R A] : Module R ↥(skewAdjoint A)

theorem IsSelfAdjoint.smul_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [AddCommGroup A] [Module R A] [StarAddMonoid R] [StarAddMonoid A] [StarModule R A] {r : R} (hr : r ∈ skewAdjoint R) {a : A} (ha : IsSelfAdjoint a) : r • a ∈ skewAdjoint A

Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a skew-adjoint element.

theorem isSelfAdjoint_smul_of_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [AddCommGroup A] [Module R A] [StarAddMonoid R] [StarAddMonoid A] [StarModule R A] {r : R} (hr : r ∈ skewAdjoint R) {a : A} (ha : a ∈ skewAdjoint A) : IsSelfAdjoint (r • a)

Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a self-adjoint element.

instance IsStarNormal.zero {R : Type u_1} [NonUnitalNonAssocSemiring R] [StarAddMonoid R] : IsStarNormal 0

instance IsStarNormal.one {R : Type u_1} [MulOneClass R] [StarMul R] : IsStarNormal 1

instance IsStarNormal.star {R : Type u_1} [Mul R] [StarMul R] {x : R} [IsStarNormal x] : IsStarNormal (star x)

instance IsStarNormal.neg {R : Type u_1} [NonUnitalNonAssocRing R] [StarAddMonoid R] {x : R} [IsStarNormal x] : IsStarNormal (-x)

instance IsStarNormal.val_inv {R : Type u_1} [Monoid R] [StarMul R] {x : Rˣ} [IsStarNormal ↑x] : IsStarNormal ↑x⁻¹

instance IsStarNormal.map {F : Type u_3} {R : Type u_4} {S : Type u_5} [Mul R] [Star R] [Mul S] [Star S] [FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] : IsStarNormal (f r)

instance IsStarNormal.smul {R : Type u_3} {A : Type u_4} [SMul R A] [Star R] [Star A] [Mul A] [StarModule R A] [SMulCommClass R A A] [IsScalarTower R A A] (r : R) (a : A) [ha : IsStarNormal a] : IsStarNormal (r • a)

@[instance 100]

instance TrivialStar.isStarNormal {R : Type u_1} [Mul R] [StarMul R] [TrivialStar R] {x : R} : IsStarNormal x

@[instance 100]

instance CommMonoid.isStarNormal {R : Type u_1} [CommMonoid R] [StarMul R] {x : R} : IsStarNormal x

theorem Commute.isStarNormal_add {R : Type u_1} [NonUnitalNonAssocSemiring R] [StarRing R] {a b : R} (hab : Commute a (star b)) [ha : IsStarNormal a] [hb : IsStarNormal b] : IsStarNormal (a + b)

theorem Commute.isStarNormal_sub {R : Type u_1} [NonUnitalNonAssocRing R] [StarRing R] {a b : R} (hab : Commute a (star b)) [ha : IsStarNormal a] [hb : IsStarNormal b] : IsStarNormal (a - b)

instance IsStarNormal.one_add {R : Type u_1} [NonAssocSemiring R] [StarRing R] {a : R} [ha : IsStarNormal a] : IsStarNormal (1 + a)

instance IsStarNormal.one_sub {R : Type u_1} [NonAssocRing R] [StarRing R] {a : R} [ha : IsStarNormal a] : IsStarNormal (1 - a)

theorem Pi.isSelfAdjoint {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} : IsSelfAdjoint f ↔ ∀ (i : ι), IsSelfAdjoint (f i)

theorem IsSelfAdjoint.apply {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} : IsSelfAdjoint f → ∀ (i : ι), IsSelfAdjoint (f i)

Alias of the forward direction of Pi.isSelfAdjoint.