mathlib documentation

algebra.star.unitary

Unitary elements of a star monoid #

This file defines unitary R, where R is a star monoid, as the submonoid made of the elements that satisfy star U * U = 1 and U * star U = 1, and these form a group. This includes, for instance, unitary operators on Hilbert spaces.

See also matrix.unitary_group for specializations to unitary (matrix n n R).

Tags #

unitary

def unitary (R : Type u_1) [monoid R] [star_semigroup R] :

In a *-monoid, unitary R is the submonoid consisting of all the elements U of R such that star U * U = 1 and U * star U = 1.

Equations
Instances for unitary
theorem unitary.mem_iff {R : Type u_1} [monoid R] [star_semigroup R] {U : R} :
@[simp]
theorem unitary.star_mul_self_of_mem {R : Type u_1} [monoid R] [star_semigroup R] {U : R} (hU : U unitary R) :
@[simp]
theorem unitary.mul_star_self_of_mem {R : Type u_1} [monoid R] [star_semigroup R] {U : R} (hU : U unitary R) :
theorem unitary.star_mem {R : Type u_1} [monoid R] [star_semigroup R] {U : R} (hU : U unitary R) :
@[simp]
theorem unitary.star_mem_iff {R : Type u_1} [monoid R] [star_semigroup R] {U : R} :
@[protected, instance]
def unitary.has_star {R : Type u_1} [monoid R] [star_semigroup R] :
Equations
@[simp, norm_cast]
theorem unitary.coe_star {R : Type u_1} [monoid R] [star_semigroup R] {U : (unitary R)} :
theorem unitary.coe_star_mul_self {R : Type u_1} [monoid R] [star_semigroup R] (U : (unitary R)) :
theorem unitary.coe_mul_star_self {R : Type u_1} [monoid R] [star_semigroup R] (U : (unitary R)) :
@[simp]
theorem unitary.star_mul_self {R : Type u_1} [monoid R] [star_semigroup R] (U : (unitary R)) :
@[simp]
theorem unitary.mul_star_self {R : Type u_1} [monoid R] [star_semigroup R] (U : (unitary R)) :
@[protected, instance]
def unitary.group {R : Type u_1} [monoid R] [star_semigroup R] :
Equations
@[protected, instance]
def unitary.inhabited {R : Type u_1} [monoid R] [star_semigroup R] :
Equations
theorem unitary.star_eq_inv {R : Type u_1} [monoid R] [star_semigroup R] (U : (unitary R)) :
@[simp]
theorem unitary.coe_to_units_apply {R : Type u_1} [monoid R] [star_semigroup R] (x : (unitary R)) :
def unitary.to_units {R : Type u_1} [monoid R] [star_semigroup R] :

The unitary elements embed into the units.

Equations
theorem unitary.mem_iff_star_mul_self {R : Type u_1} [comm_monoid R] [star_semigroup R] {U : R} :
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [comm_monoid R] [star_semigroup R] {U : R} :
@[norm_cast]
theorem unitary.coe_inv {R : Type u_1} [group_with_zero R] [star_semigroup R] (U : (unitary R)) :
@[norm_cast]
theorem unitary.coe_div {R : Type u_1} [group_with_zero R] [star_semigroup R] (U₁ U₂ : (unitary R)) :
(U₁ / U₂) = U₁ / U₂
@[norm_cast]
theorem unitary.coe_zpow {R : Type u_1} [group_with_zero R] [star_semigroup R] (U : (unitary R)) (z : ) :
(U ^ z) = U ^ z
@[protected, instance]
def unitary.has_neg {R : Type u_1} [ring R] [star_ring R] :
Equations
@[norm_cast]
theorem unitary.coe_neg {R : Type u_1} [ring R] [star_ring R] (U : (unitary R)) :
@[protected, instance]
Equations