# Documentation

Mathlib.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.UnitaryGroup for specializations to unitary (Matrix n n R).

## Tags #

unitary

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

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.

Instances For
theorem unitary.mem_iff {R : Type u_1} [] [] {U : R} :
U star U * U = 1 U * star U = 1
@[simp]
theorem unitary.star_mul_self_of_mem {R : Type u_1} [] [] {U : R} (hU : U ) :
star U * U = 1
@[simp]
theorem unitary.mul_star_self_of_mem {R : Type u_1} [] [] {U : R} (hU : U ) :
U * star U = 1
theorem unitary.star_mem {R : Type u_1} [] [] {U : R} (hU : U ) :
@[simp]
theorem unitary.star_mem_iff {R : Type u_1} [] [] {U : R} :
@[simp]
theorem unitary.coe_star {R : Type u_1} [] [] {U : { x // x }} :
↑(star U) = star U
theorem unitary.coe_star_mul_self {R : Type u_1} [] [] (U : { x // x }) :
star U * U = 1
theorem unitary.coe_mul_star_self {R : Type u_1} [] [] (U : { x // x }) :
U * ↑(star U) = 1
@[simp]
theorem unitary.star_mul_self {R : Type u_1} [] [] (U : { x // x }) :
star U * U = 1
@[simp]
theorem unitary.mul_star_self {R : Type u_1} [] [] (U : { x // x }) :
U * star U = 1
theorem unitary.star_eq_inv {R : Type u_1} [] [] (U : { x // x }) :
theorem unitary.star_eq_inv' {R : Type u_1} [] [] :
star = Inv.inv
@[simp]
theorem unitary.val_inv_toUnits_apply {R : Type u_1} [] [] (x : { x // x }) :
(unitary.toUnits x)⁻¹ = x⁻¹
@[simp]
theorem unitary.val_toUnits_apply {R : Type u_1} [] [] (x : { x // x }) :
↑(unitary.toUnits x) = x
def unitary.toUnits {R : Type u_1} [] [] :
{ x // x } →* Rˣ

The unitary elements embed into the units.

Instances For
theorem unitary.to_units_injective {R : Type u_1} [] [] :
Function.Injective unitary.toUnits
theorem unitary.mem_iff_star_mul_self {R : Type u_1} [] [] {U : R} :
U star U * U = 1
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [] [] {U : R} :
U U * star U = 1
theorem unitary.coe_inv {R : Type u_1} [] [] (U : { x // x }) :
U⁻¹ = (U)⁻¹
theorem unitary.coe_div {R : Type u_1} [] [] (U₁ : { x // x }) (U₂ : { x // x }) :
↑(U₁ / U₂) = U₁ / U₂
theorem unitary.coe_zpow {R : Type u_1} [] [] (U : { x // x }) (z : ) :
↑(U ^ z) = U ^ z
theorem unitary.coe_neg {R : Type u_1} [Ring R] [] (U : { x // x }) :
↑(-U) = -U