unitary.star_mem
theorem unitary.star_mem :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → star U ∈ unitary R
This theorem states that for any type `R` which is a monoid with additional structure given by a `StarMul` operation, if `U` is an element of the unitary submonoid of `R` (which means `U` satisfies the property that the star operation followed by multiplication with `U` yields the identity both ways), then the star of `U` is also an element of the unitary submonoid of `R`. In other words, if a `U` belongs to the unitary submonoid, its star version does too.
More concisely: If `U` is an element of the unitary submonoid of a monoid `R` with a `StarMul` operation, then the star of `U` is also an element of the unitary submonoid of `R`.
|
unitary.coe_star_mul_self
theorem unitary.coe_star_mul_self :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (U : ↥(unitary R)), star ↑U * ↑U = 1
This theorem states that for any type `R` that is a monoid with a `StarMul` operation, and for any element `U` belonging to the submonoid of `R` defined by the `unitary` operation, the product of the star of `U` and `U` itself is equal to one. In other words, it confirms that the defining property of unitary elements (i.e., `star U * U = 1`) holds for all elements in the unitary submonoid of `R`.
More concisely: For any monoid `R` with a `StarMul` operation and any unitary element `U` in `R`, `StarU * U = 1`.
|
unitary.mul_star_self_of_mem
theorem unitary.mul_star_self_of_mem :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → U * star U = 1
This theorem states that for any type `R` that is a monoid and has a star multiplication operation, if an element `U` of `R` belongs to the submonoid of `R` called `unitary`, then the product of `U` and the star-multiplication of `U` is equal to 1. In other words, in any star-monoid, if a given element is in the unitary submonoid, then it satisfies the unitary property that its multiplication with its star-multiplication results in the multiplicative identity element (1).
More concisely: Given a monoid `R` with star multiplication operation, if `U` is an element of the unitary submonoid of `R`, then `U * U^* = 1`.
|
unitary.star_mul_self_of_mem
theorem unitary.star_mul_self_of_mem :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → star U * U = 1
This theorem states that for any type `R` that is a monoid with the additional structure `StarMul`, if `U` is an element of the submonoid `unitary R` (which consists of all elements `U` such that `star U * U = 1` and `U * star U = 1`), then the property `star U * U = 1` holds. In other words, for any unitary element `U`, the product of its star and itself equals the multiplicative identity of the monoid.
More concisely: For any monoid `R` with `StarMul` structure and any `U` in the unitary submonoid, `star U * U = 1`.
|
unitary.mem_iff
theorem unitary.mem_iff :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1
The theorem `unitary.mem_iff` states that for any type `R` with a `Monoid` and `StarMul` structure, and for any element `U` of `R`, `U` is a member of the `unitary` submonoid of `R` if and only if the product of `star U` and `U` equals 1 and the product of `U` and `star U` equals 1. In other words, an element `U` belongs to the set of unitary elements of `R` precisely when `star U * U = 1` and `U * star U = 1`.
More concisely: An element `U` of a type `R` equipped with `Monoid` and `StarMul` structures belongs to the unitary submonoid if and only if `star U * U = 1` and `U * star U = 1`.
|