# mathlib3documentation

algebra.star.unitary

# Unitary elements of a star monoid #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]  :

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] {U : R} :
U = 1 = 1
@[simp]
theorem unitary.star_mul_self_of_mem {R : Type u_1} [monoid R] {U : R} (hU : U ) :
= 1
@[simp]
theorem unitary.mul_star_self_of_mem {R : Type u_1} [monoid R] {U : R} (hU : U ) :
= 1
theorem unitary.star_mem {R : Type u_1} [monoid R] {U : R} (hU : U ) :
@[simp]
theorem unitary.star_mem_iff {R : Type u_1} [monoid R] {U : R} :
U
@[protected, instance]
def unitary.has_star {R : Type u_1} [monoid R]  :
Equations
@[simp, norm_cast]
theorem unitary.coe_star {R : Type u_1} [monoid R] {U : (unitary R)} :
theorem unitary.coe_star_mul_self {R : Type u_1} [monoid R] (U : (unitary R)) :
= 1
theorem unitary.coe_mul_star_self {R : Type u_1} [monoid R] (U : (unitary R)) :
= 1
@[simp]
theorem unitary.star_mul_self {R : Type u_1} [monoid R] (U : (unitary R)) :
= 1
@[simp]
theorem unitary.mul_star_self {R : Type u_1} [monoid R] (U : (unitary R)) :
= 1
@[protected, instance]
def unitary.group {R : Type u_1} [monoid R]  :
Equations
@[protected, instance]
def unitary.has_involutive_star {R : Type u_1} [monoid R]  :
Equations
@[protected, instance]
def unitary.star_semigroup {R : Type u_1} [monoid R]  :
Equations
@[protected, instance]
def unitary.inhabited {R : Type u_1} [monoid R]  :
Equations
theorem unitary.star_eq_inv {R : Type u_1} [monoid R] (U : (unitary R)) :
theorem unitary.star_eq_inv' {R : Type u_1} [monoid R]  :
@[simp]
theorem unitary.coe_to_units_apply {R : Type u_1} [monoid R] (x : (unitary R)) :
= x
def unitary.to_units {R : Type u_1} [monoid R]  :

The unitary elements embed into the units.

Equations
@[simp]
theorem unitary.coe_inv_to_units_apply {R : Type u_1} [monoid R] (x : (unitary R)) :
theorem unitary.to_units_injective {R : Type u_1} [monoid R]  :
@[protected, instance]
def unitary.comm_group {R : Type u_1} [comm_monoid R]  :
Equations
theorem unitary.mem_iff_star_mul_self {R : Type u_1} [comm_monoid R] {U : R} :
U = 1
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [comm_monoid R] {U : R} :
U = 1
@[norm_cast]
theorem unitary.coe_inv {R : Type u_1} (U : (unitary R)) :
@[norm_cast]
theorem unitary.coe_div {R : Type u_1} (U₁ U₂ : (unitary R)) :
(U₁ / U₂) = U₁ / U₂
@[norm_cast]
theorem unitary.coe_zpow {R : Type u_1} (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]
def unitary.has_distrib_neg {R : Type u_1} [ring R] [star_ring R] :
Equations