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 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 : R} {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.starHom_apply {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_starHom_apply {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)

@[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 : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x + y)

@[deprecated]

theorem IsSelfAdjoint.bit0 {R : Type u_1} [AddMonoid R] [StarAddMonoid R] {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint (bit0 x)

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 : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x - y)

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

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.isStarNormal {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) : IsStarNormal x

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

@[deprecated]

theorem IsSelfAdjoint.bit1 {R : Type u_1} [Semiring R] [StarRing R] {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint (bit1 x)

@[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 : ℕ) [Nat.AtLeastTwo n] : IsSelfAdjoint (OfNat.ofNat n)

theorem IsSelfAdjoint.mul {R : Type u_1} [CommSemigroup R] [StarMul R] {x : R} {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} [DivisionSemiring R] [StarRing R] {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint x⁻¹

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

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 : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y)

theorem IsSelfAdjoint.smul {R : Type u_1} {A : Type u_2} [Star R] [AddMonoid A] [StarAddMonoid A] [SMul R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) {x : A} (hx : IsSelfAdjoint x) : IsSelfAdjoint (r • 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 = { toAddSubmonoid := { toAddSubsemigroup := { 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 = { toAddSubmonoid := { toAddSubsemigroup := { 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.instInhabitedSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint {R : Type u_1} [AddGroup R] [StarAddMonoid R] : Inhabited ↥(selfAdjoint R)

Equations

• selfAdjoint.instInhabitedSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { default := 0 }

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• selfAdjoint.instQSMul = { smul := fun (a : ℚ) (x : ↥(selfAdjoint R)) => { val := a • ↑x, property := ⋯ } }

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

instance selfAdjoint.instSMulSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint {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.instSMulSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { smul := fun (r : R) (x : ↥(selfAdjoint A)) => { val := r • ↑x, property := ⋯ } }

@[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.instMulActionSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint {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.instMulActionSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = Function.Injective.mulAction Subtype.val ⋯ ⋯

instance selfAdjoint.instDistribMulActionSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjointToAddMonoidToAddMonoidToSubNegMonoidToAddSubmonoid {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

• One or more equations did not get rendered due to their size.

instance selfAdjoint.instModuleSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSelfAdjointToAddCommMonoidToAddCommMonoidToAddSubmonoid {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

• One or more equations did not get rendered due to their size.

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.instInhabitedSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjoint {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] : Inhabited ↥(skewAdjoint R)

Equations

• skewAdjoint.instInhabitedSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjoint = { default := 0 }

@[deprecated]

theorem skewAdjoint.bit0_mem {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : R} (hx : x ∈ skewAdjoint R) : bit0 x ∈ 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.instIsStarNormalToMulToNonUnitalNonAssocRingToNonAssocRingToStarToInvolutiveStarToAddMonoidToAddMonoidWithOneToAddGroupWithOneToStarAddMonoidToNonUnitalNonAssocSemiringValMemSetInstMembershipSetCoeAddSubgroupToAddGroupToAddCommGroupInstSetLikeAddSubgroupSkewAdjoint {R : Type u_1} [Ring R] [StarRing R] (x : ↥(skewAdjoint R)) : IsStarNormal ↑x

Equations

• ⋯ = ⋯

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.instSMulSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjoint {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.instSMulSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjoint = { smul := fun (r : R) (x : ↥(skewAdjoint A)) => { val := r • ↑x, property := ⋯ } }

@[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.instDistribMulActionSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjointToAddMonoidToAddMonoidToSubNegMonoidToAddSubmonoid {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

• One or more equations did not get rendered due to their size.

instance skewAdjoint.instModuleSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjointToAddCommMonoidToAddCommMonoidToAddSubmonoid {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

• One or more equations did not get rendered due to their size.

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} [Semiring R] [StarRing R] : IsStarNormal 0

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.