IsSelfAdjoint.all
theorem IsSelfAdjoint.all : ∀ {R : Type u_1} [inst : Star R] [inst_1 : TrivialStar R] (r : R), IsSelfAdjoint r := by
sorry
The theorem `IsSelfAdjoint.all` states that for any type `R` equipped with a `Star` operation and a trivial `Star` operation (where the `Star` of any element is the element itself), any element `r` of `R` is self-adjoint. Being self-adjoint is defined as an element being equal to its star, i.e., the star of the element is the element itself. This makes sense in this case, as the `Star` operation is assumed to be trivial, and therefore always returns the original element.
More concisely: For any type `R` with a trivial `Star` operation, every element `r` in `R` is self-adjoint.
|
Mathlib.Algebra.Star.SelfAdjoint._auxLemma.19
theorem Mathlib.Algebra.Star.SelfAdjoint._auxLemma.19 :
∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute (-a) b = True
The theorem `Mathlib.Algebra.Star.SelfAdjoint._auxLemma.19` states that for any type `S` equipped with a multiplication operation, and for any element `a` of `S`, it is always true that `a` commutes with itself. In other words, for any element `a` in a structure that supports multiplication, the product of `a` with itself is the same regardless of the order of multiplication, i.e., `a * a = a * a`.
More concisely: For any type equipped with multiplication, the self-multiplication of any element is commutative, i.e., `a * a = a * a` for all `a` in the type.
|
IsSelfAdjoint.apply
theorem IsSelfAdjoint.apply :
∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Star (α i)] {f : (i : ι) → α i},
IsSelfAdjoint f → ∀ (i : ι), IsSelfAdjoint (f i)
The theorem `IsSelfAdjoint.apply` states that given an index type `ι`, a type function `α` mapping from `ι` to some type, a star operation on each type given by `α i` for all `i` in `ι`, and a function `f` from `ι` to `α i`, if `f` is self-adjoint (in the sense that its star is equal to itself), then for any index `i` in `ι`, the value `f i` is also self-adjoint. In other words, if a function is self-adjoint, then each of its values at any index is also self-adjoint.
More concisely: If `f` is a self-adjoint function on an index type `ι` with respect to a given star operation on each index's type `α i`, then each value `f i` is self-adjoint.
|
isSelfAdjoint_zero
theorem isSelfAdjoint_zero : ∀ (R : Type u_1) [inst : AddMonoid R] [inst_1 : StarAddMonoid R], IsSelfAdjoint 0 := by
sorry
The theorem `isSelfAdjoint_zero` states that for any type `R` which is an additive monoid and a star additive monoid (i.e., it has a star operation that interacts well with addition), the zero element of `R` is self-adjoint. In other words, applying the star operation to zero gives us zero itself. In mathematical terms, if `R` is a star add monoid, then `0* = 0`.
More concisely: In a star additive monoid `R`, the zero element is self-adjoint, i.e., `0* = 0`.
|
IsSelfAdjoint.smul_mem_skewAdjoint
theorem IsSelfAdjoint.smul_mem_skewAdjoint :
∀ {R : Type u_1} {A : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup A] [inst_2 : Module R A]
[inst_3 : StarAddMonoid R] [inst_4 : StarAddMonoid A] [inst_5 : StarModule R A] {r : R},
r ∈ skewAdjoint R → ∀ {a : A}, IsSelfAdjoint a → r • a ∈ skewAdjoint A
The theorem `IsSelfAdjoint.smul_mem_skewAdjoint` states that for any types `R` and `A` where `R` is a ring, `A` is an additive commutative group, `A` is a module over `R`, both `R` and `A` are star add monoids and star acts linearly on `A`, if `r` is an element from `R` that is skew-adjoint (i.e., its star equals its negative) and `a` is an element from `A` that is self-adjoint (i.e., equals to its star), then the scalar multiplication of `r` and `a` is also a skew-adjoint element of `A`.
More concisely: If `r` is a skew-adjoint element in a ring `R` and `a` is a self-adjoint element in an additive commutative group `A` that is a module over `R`, then the scalar multiplication `r * a` is skew-adjoint in `A`.
|
IsSelfAdjoint.star_mul_self
theorem IsSelfAdjoint.star_mul_self :
∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] (x : R), IsSelfAdjoint (star x * x)
This theorem states that for any type `R` that supports multiplication (`Mul`) and star multiplication (`StarMul`), any element `x` of `R` is self-adjoint when it's the product of its star version and itself. In mathematical terms, if we denote the star of an element `x` as `x*`, then `x* * x` is self-adjoint, that is, `(x* * x)* = x* * x`.
More concisely: For any type `R` with multiplication and star multiplication, and for any element `x` in `R`, `x* * x` equals the self-adjoint version of `x* * x`, i.e., `(x* * x) = x* * x`.
|
star_comm_self'
theorem star_comm_self' :
∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] (x : R) [inst_2 : IsStarNormal x], star x * x = x * star x := by
sorry
This theorem states that for any type `R` equipped with a multiplication operation (`Mul R`) and a `star` operation (`Star R`), and for any element `x` of `R` that is star-normal (`IsStarNormal x`), the product of `star x` and `x` is equal to the product of `x` and `star x`. In other words, the multiplication of `star x` and `x` commutes in the context of star-normal elements.
More concisely: For any commutative ring `R` with a `star` operation, and for any star-normal element `x` in `R`, we have `(star x) * x = x * (star x)`.
|
skewAdjoint.mem_iff
theorem skewAdjoint.mem_iff :
∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : StarAddMonoid R] {x : R}, x ∈ skewAdjoint R ↔ star x = -x := by
sorry
This theorem states that, for any type 'R' equipped with a structure of an additive commutative group and a star additive monoid, an element 'x' of 'R' belongs to the set of skew-adjoint elements if and only if the star of 'x' is equal to the additive inverse of 'x'. In other words, the 'star' of an element is its negative if and only if that element is skew-adjoint.
More concisely: An element x of an additive commutative group R equipped with a star additive monoid is skew-adjoint if and only if the star of x is the additive inverse of x.
|
Mathlib.Algebra.Star.SelfAdjoint._auxLemma.17
theorem Mathlib.Algebra.Star.SelfAdjoint._auxLemma.17 :
∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : TrivialStar R] [inst_2 : AddGroup A]
[inst_3 : StarAddMonoid A] [inst_4 : SMul R A] [inst_5 : StarModule R A] (r : R) (x : ↥(selfAdjoint A)),
r • ↑x = ↑(r • x)
The theorem `Mathlib.Algebra.Star.SelfAdjoint._auxLemma.17` states that for any type `R` equipped with the structure of an additive commutative group and a star additive monoid, and for any element `x` of `R`, `x` belongs to the skew-adjoint elements of `R` if and only if the star of `x` equals the additive inverse of `x`. Here, "skew-adjoint elements" refers to elements whose "star" (a certain unary operation) equals their own negatives in the additive sense.
More concisely: For any element `x` in a type `R` with an additive commutative group and a star additive monoid structure, `x` is skew-adjoint if and only if the star of `x` is equal to the additive inverse of `x`.
|
selfAdjoint.val_smul
theorem selfAdjoint.val_smul :
∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : TrivialStar R] [inst_2 : AddGroup A]
[inst_3 : StarAddMonoid A] [inst_4 : SMul R A] [inst_5 : StarModule R A] (r : R) (x : ↥(selfAdjoint A)),
↑(r • x) = r • ↑x
The theorem `selfAdjoint.val_smul` states that for any type `R` equipped with a star operation and a trivial star operation, and for any type `A` equipped with an additive group structure, a star-addition operation, scalar multiplication, and a star module structure, the scalar multiplication of any scalar `r` from `R` and any element `x` from the set of self-adjoint elements in `A` is unchanged when the operation is carried out within the set of self-adjoint elements or in the larger set `A`. More precisely, if `x` is a self-adjoint element of `A` and `r` is a scalar, then the scalar multiplication of `r` and `x` in the subgroup of self-adjoint elements is equal to the scalar multiplication of `r` and `x` in the group `A`.
More concisely: For any self-adjoint element `x` in an additive group `A` equipped with a star operation and a star module structure over a commutative ring `R` with a trivial star operation, and for any scalar `r` in `R`, the scalar multiplication `r * x` is the same in the subgroup of self-adjoint elements as in `A`.
|
IsSelfAdjoint.star_eq
theorem IsSelfAdjoint.star_eq : ∀ {R : Type u_1} [inst : Star R] {x : R}, IsSelfAdjoint x → star x = x
This theorem states that for any type `R` that has a `Star` operation, if an element `x` of `R` is self-adjoint, then the star of `x` is equal to `x`. The condition of being self-adjoint is defined as an element being equal to its star. In mathematical terms, this would be equivalent to saying for a given element `x` in a star-algebra `R`, if `x` is self-adjoint (meaning that `x` is equal to its conjugate or adjoint), then the adjoint operation on `x` results in `x` itself.
More concisely: For any self-adjoint element `x` in a star-algebra `R`, `x` equals its adjoint `x*`.
|
IsStarNormal.star_comm_self
theorem IsStarNormal.star_comm_self :
∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] {x : R} [self : IsStarNormal x], Commute (star x) x
This theorem states that for any type `R` that has a multiplication operation and a star operation, and for any element `x` of `R` that is a star-normal element, the star of `x` commutes with `x`. In other words, `(star x) * x = x * (star x)`. Here, `star` is an operation often seen in the context of star algebras, and a star-normal element is one that satisfies certain properties with respect to this operation. The `Commute` function is used to express the commutativity of two elements.
More concisely: For any type `R` with multiplication and star operation, and for any star-normal element `x` in `R`, `star x * x = x * star x`.
|
IsSelfAdjoint.starHom_apply
theorem IsSelfAdjoint.starHom_apply :
∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Star R] [inst_1 : Star S] [inst_2 : FunLike F R S]
[inst_3 : StarHomClass F R S] {x : R}, IsSelfAdjoint x → ∀ (f : F), IsSelfAdjoint (f x)
The theorem `IsSelfAdjoint.starHom_apply` states that for all types `F`, `R`, `S`, given the type `R` and `S` have a `Star` instance, `F` is a function from `R` to `S`, and there exists a `StarHomClass` instance for `F`, `R` and `S`, then for any self-adjoint element `x` of type `R`, the application of a function `f` of type `F` on `x` will also be a self-adjoint element. Here, an element is considered self-adjoint if it is equal to its star, and a `StarHomClass` indicates that the function preserves the star operation.
More concisely: If `F` is a star-preserving function from a self-adjoint element in a *-algebra `R` to a *-algebra `S`, then the image of the self-adjoint element under `F` is also self-adjoint.
|
Mathlib.Algebra.Star.SelfAdjoint._auxLemma.5
theorem Mathlib.Algebra.Star.SelfAdjoint._auxLemma.5 :
∀ {R : Type u_1} [inst : Star R] {x : R}, IsSelfAdjoint x = (star x = x)
The theorem `Mathlib.Algebra.Star.SelfAdjoint._auxLemma.5` states that for any type `R` equipped with a star operation (denoted by `Star R`), and any element `x` of `R`, this element `x` is self-adjoint (as defined by the function `IsSelfAdjoint`) if and only if `x` is equal to its star operation (`star x = x`). In other words, the theorem is saying that an element is self-adjoint if it is equal to its own complex conjugate in the context of complex numbers.
More concisely: An element in a type equipped with a star operation is self-adjoint if and only if it is equal to its complex conjugate (star operation).
|
IsSelfAdjoint.commute_iff
theorem IsSelfAdjoint.commute_iff :
∀ {R : Type u_3} [inst : Mul R] [inst_1 : StarMul R] {x y : R},
IsSelfAdjoint x → IsSelfAdjoint y → (Commute x y ↔ IsSelfAdjoint (x * y))
This theorem states that for any type `R` that supports multiplication (`Mul`) and the star operation (`StarMul`), and given any two elements `x` and `y` of `R` that are self-adjoint (meaning that each element is equal to its own star), these two elements commute (i.e., `x * y = y * x`) if and only if their product is also self-adjoint.
More concisely: For any commutative ring `R` with self-adjoint elements `x` and `y`, `x * y` is self-adjoint if and only if `x * y = y * x`.
|
isSelfAdjoint_smul_of_mem_skewAdjoint
theorem isSelfAdjoint_smul_of_mem_skewAdjoint :
∀ {R : Type u_1} {A : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup A] [inst_2 : Module R A]
[inst_3 : StarAddMonoid R] [inst_4 : StarAddMonoid A] [inst_5 : StarModule R A] {r : R},
r ∈ skewAdjoint R → ∀ {a : A}, a ∈ skewAdjoint A → IsSelfAdjoint (r • a)
The theorem states that for any ring `R` and additive commutative group `A` with a module structure over `R` and both having star add monoid structures, and if `A` also possesses a star module structure, then scalar multiplication of a skew-adjoint element from `R` by a skew-adjoint element from `A` results in a self-adjoint element. Here, a skew-adjoint element is an element whose star is its additive inverse, and a self-adjoint element is an element that is equal to its own star.
More concisely: For any ring `R`, additive commutative group `A` with an `R`-module and star add monoid structures, if `A` also has a star module structure and both `R` and `A` contain only skew-adjoint elements, then scalar multiplication of two such elements results in a self-adjoint element.
|