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.

Equations

• IsSelfAdjoint x = (star x = x)

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)

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} [Semiring R] [StarRing R] (n : ℕ) : IsSelfAdjoint ↑n

@[simp]

theorem IsSelfAdjoint.ofNat {R : Type u_1} [Semiring 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⁻¹

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⁻¹

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.

Equations

• selfAdjoint R = { carrier := {x : R | IsSelfAdjoint x}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

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.

Equations

• skewAdjoint R = { carrier := {x : R | star x = -x}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

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

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

Equations

• selfAdjoint.instInhabitedSubtypeMemAddSubgroup = { default := 0 }

@[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

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

Equations

• selfAdjoint.instOneSubtypeMemAddSubgroup = { one := ⟨1, ⋯⟩ }

@[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)

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

Equations

• selfAdjoint.instNatCastSubtypeMemAddSubgroup = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩ }

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

Equations

• selfAdjoint.instIntCastSubtypeMemAddSubgroup = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }

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

Equations

• selfAdjoint.instPowSubtypeMemAddSubgroupNat = { pow := fun (x : ↥(selfAdjoint R)) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

@[simp]

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

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

Equations

• selfAdjoint.instMulSubtypeMemAddSubgroup = { mul := fun (x y : ↥(selfAdjoint R)) => ⟨↑x * ↑y, ⋯⟩ }

@[simp]

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

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

Equations

• selfAdjoint.instCommRingSubtypeMemAddSubgroup = Function.Injective.commRing (fun (a : ↥(selfAdjoint R)) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• selfAdjoint.instInvSubtypeMemAddSubgroup = { inv := fun (x : ↥(selfAdjoint R)) => ⟨(↑x)⁻¹, ⋯⟩ }

@[simp]

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

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

Equations

• selfAdjoint.instDivSubtypeMemAddSubgroup = { div := fun (x y : ↥(selfAdjoint R)) => ⟨↑x / ↑y, ⋯⟩ }

@[simp]

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

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

Equations

• selfAdjoint.instPowSubtypeMemAddSubgroupInt = { pow := fun (x : ↥(selfAdjoint R)) (z : ℤ) => ⟨↑x ^ z, ⋯⟩ }

@[simp]

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

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

Equations

• selfAdjoint.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ⟨↑q, ⋯⟩ }

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

Equations

• selfAdjoint.instRatCast = { ratCast := fun (q : ℚ) => ⟨↑q, ⋯⟩ }

@[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

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

Equations

• selfAdjoint.instSMulNNRat = { smul := fun (a : ℚ≥0) (x : ↥(selfAdjoint R)) => ⟨a • ↑x, ⋯⟩ }

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

Equations

• selfAdjoint.instSMulRat = { smul := fun (a : ℚ) (x : ↥(selfAdjoint R)) => ⟨a • ↑x, ⋯⟩ }

@[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

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

Equations

• selfAdjoint.instField = Function.Injective.field (fun (a : ↥(selfAdjoint R)) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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)

Equations

• selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule = { smul := fun (r : R) (x : ↥(selfAdjoint A)) => ⟨r • ↑x, ⋯⟩ }

@[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

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)

Equations

• selfAdjoint.instMulActionSubtypeMemAddSubgroupOfStarModule = Function.Injective.mulAction Subtype.val ⋯ ⋯

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)

Equations

• selfAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule = Function.Injective.distribMulAction (selfAdjoint A).subtype ⋯ ⋯

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)

Equations

• selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule = Function.Injective.module R (selfAdjoint A).subtype ⋯ ⋯

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

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

Equations

• skewAdjoint.instInhabitedSubtypeMemAddSubgroup = { default := 0 }

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

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)

Equations

• skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule = { smul := fun (r : R) (x : ↥(skewAdjoint A)) => ⟨r • ↑x, ⋯⟩ }

@[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

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)

Equations

• skewAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule = Function.Injective.distribMulAction (skewAdjoint A).subtype ⋯ ⋯

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)

Equations

• skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule = Function.Injective.module R (skewAdjoint A).subtype ⋯ ⋯

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.