[GOAL]
R : Type u_1
A : Type u_2
inst✝ : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x
[PROOFSTEP]
simpa only [IsSelfAdjoint, star_star] using eq_comm
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
⊢ IsSelfAdjoint (star x * x)
[PROOFSTEP]
simp only [IsSelfAdjoint, star_mul, star_star]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
⊢ IsSelfAdjoint (x * star x)
[PROOFSTEP]
simpa only [star_star] using star_mul_self (star x)
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_add, hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (_root_.bit0 x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_bit0, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_sub, hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (x + star x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (star x + x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (z * x * star z)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
⊢ Commute (star x) x
[PROOFSTEP]
simp only [Commute, SemiconjBy, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
n : ℕ
⊢ IsSelfAdjoint (x ^ n)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : StarRing R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (_root_.bit1 x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_bit1, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : CommSemigroup R
inst✝ : StarSemigroup R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : DivisionSemiring R
inst✝ : StarRing R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_inv', hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : DivisionSemiring R
inst✝ : StarRing R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_zpow₀, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_div', hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Star R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : SMul R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
x : A
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_smul, hr.star_eq, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
⊢ star (x + y) = -(x + y)
[PROOFSTEP]
rw [star_add x y, hx, hy, neg_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
⊢ star 0 = -0
[PROOFSTEP]
simp only [star_zero, neg_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
hx : star x = -x
⊢ star (-x) = - -x
[PROOFSTEP]
simp only [hx, star_neg]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ selfAdjoint R ↔ star x = x
[PROOFSTEP]
rw [← AddSubgroup.mem_carrier]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).toAddSubmonoid.toAddSubsemigroup.carrier ↔ star x = x
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : { x // x ∈ selfAdjoint R }
⊢ a • ↑x ∈ selfAdjoint R
[PROOFSTEP]
rw [Rat.smul_def]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : { x // x ∈ selfAdjoint R }
⊢ ↑a * ↑x ∈ selfAdjoint R
[PROOFSTEP]
exact IsSelfAdjoint.mul (isSelfAdjoint_ratCast a) x.prop
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ skewAdjoint R ↔ star x = -x
[PROOFSTEP]
rw [← AddSubgroup.mem_carrier]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).toAddSubmonoid.toAddSubsemigroup.carrier ↔ star x = -x
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
hx : x ∈ skewAdjoint R
⊢ bit0 x ∈ skewAdjoint R
[PROOFSTEP]
rw [mem_iff, star_bit0, mem_iff.mp hx, bit0, bit0, neg_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ z * x * star z ∈ skewAdjoint R
[PROOFSTEP]
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ star z * x * z ∈ skewAdjoint R
[PROOFSTEP]
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
⊢ Commute (star x) x
[PROOFSTEP]
simp only [mem_iff] at hx 
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x
[PROOFSTEP]
simp only [hx, Commute.neg_left, Commute.refl]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁶ : Star R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : Monoid R
inst✝¹ : DistribMulAction R A
inst✝ : StarModule R A
r : R
x : A
h : x ∈ skewAdjoint A
⊢ r • x ∈ skewAdjoint A
[PROOFSTEP]
rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : StarRing R
⊢ Commute (star 0) 0
[PROOFSTEP]
simp only [Commute.refl, star_comm_self, star_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ Commute (star 1) 1
[PROOFSTEP]
simp only [Commute.refl, star_comm_self, star_one]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
x : R
inst✝ : IsStarNormal x
⊢ star (star x) * star x = star x * star (star x)
[PROOFSTEP]
rw [star_star, star_comm_self']
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
inst✝ : TrivialStar R
x : R
⊢ Commute (star x) x
[PROOFSTEP]
rw [star_trivial]
