# 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

source
def unitary (R : Type u_1) [Monoid R] [StarMul R] :
Submonoid 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

- unitary R = { carrier := {U : R | star U * U = 1 ∧ U * star U = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source
theorem Unitary.mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :
U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1
source
@[simp]
theorem Unitary.star_mul_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :
star U * U = 1
source
@[simp]
theorem Unitary.mul_star_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :
U * star U = 1
source
theorem Unitary.star_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :
star U ∈ unitary R
source
@[simp]
theorem Unitary.star_mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :
star U ∈ unitary R ↔ U ∈ unitary R
source
instance Unitary.instStarSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
Star ↥(unitary R)
Equations

- Unitary.instStarSubtypeMemSubmonoidUnitary = { star := fun (U : ↥(unitary R)) => ⟨star ↑U, ⋯⟩ }

source
@[simp]
theorem Unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : ↥(unitary R)} :
↑(star U) = star ↑U
source
theorem Unitary.coe_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
star ↑U * ↑U = 1
source
theorem Unitary.coe_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
↑U * ↑(star U) = 1
source
@[simp]
theorem Unitary.star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
star U * U = 1
source
@[simp]
theorem Unitary.mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
U * star U = 1
source
instance Unitary.instGroupSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
Group ↥(unitary R)
Equations

- One or more equations did not get rendered due to their size.

source
instance Unitary.instInvolutiveStarSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
InvolutiveStar ↥(unitary R)
Equations

- Unitary.instInvolutiveStarSubtypeMemSubmonoidUnitary = { toStar := Unitary.instStarSubtypeMemSubmonoidUnitary, star_involutive := ⋯ }

source
instance Unitary.instStarMulSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
StarMul ↥(unitary R)
Equations

- Unitary.instStarMulSubtypeMemSubmonoidUnitary = { toInvolutiveStar := Unitary.instInvolutiveStarSubtypeMemSubmonoidUnitary, star_mul := ⋯ }

source
instance Unitary.instInhabitedSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
Inhabited ↥(unitary R)
Equations

- Unitary.instInhabitedSubtypeMemSubmonoidUnitary = { default := 1 }

source
theorem Unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
star U = U⁻¹
source
theorem Unitary.star_eq_inv' {R : Type u_1} [Monoid R] [StarMul R] :
star = Inv.inv
source
def Unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :
↥(unitary R) →* R ˣ

The unitary elements embed into the units.

Equations

- Unitary.toUnits = { toFun := fun (x : ↥(unitary R)) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :
↑(toUnits x)⁻¹ = ↑x⁻¹
source
@[simp]
theorem Unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :
↑(toUnits x) = ↑x
source
theorem Unitary.toUnits_injective {R : Type u_1} [Monoid R] [StarMul R] :
Function.Injective ⇑toUnits
source
theorem IsUnit.mem_unitary_iff_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
u ∈ unitary R ↔ star u * u = 1
source
theorem IsUnit.mem_unitary_iff_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
u ∈ unitary R ↔ u * star u = 1
source
theorem IsUnit.mem_unitary_of_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
star u * u = 1 → u ∈ unitary R

Alias of the reverse direction of `IsUnit.mem_unitary_iff_star_mul_self`.

source
theorem IsUnit.mem_unitary_of_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
u * star u = 1 → u ∈ unitary R

Alias of the reverse direction of `IsUnit.mem_unitary_iff_mul_star_self`.

source
theorem Unitary.isUnit_coe {R : Type u_1} [Monoid R] [StarMul R] {U : ↥(unitary R)} :
IsUnit ↑U
source
theorem Unitary.mul_left_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :
x * ↑U = y * ↑U ↔ x = y

For unitary `U` in a star-monoid `R`, `x * U = y * U` if and only if `x = y` for all `x` and `y` in `R`.

source
theorem Unitary.mul_right_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :
↑U * x = ↑U * y ↔ x = y

For unitary `U` in a star-monoid `R`, `U * x = U * y` if and only if `x = y` for all `x` and `y` in `R`.

source
theorem Unitary.mul_inv_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b
source
theorem Unitary.inv_mul_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b
source
theorem Units.unitary_eq {R : Type u_1} [Monoid R] [StarMul R] :
unitary R ˣ = Submonoid.comap (coeHom R) (unitary R)
source
theorem Units.mul_inv_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : R ˣ) :
↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b

In a star monoid, the product `a * b⁻¹` of units is unitary if `star a * a = star b * b`.

source
theorem Units.inv_mul_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : R ˣ) :
↑a⁻¹ * ↑b ∈ unitary R ↔ a * star a = b * star b

In a star monoid, the product `a⁻¹ * b` of units is unitary if `a * star a = b * star b`.

source
instance Unitary.instIsStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : ↥(unitary R)) :
IsStarNormal u
source
instance Unitary.coe_isStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : ↥(unitary R)) :
IsStarNormal ↑u
source
theorem isStarNormal_of_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : u ∈ unitary R) :
IsStarNormal u
source
theorem Unitary.inv_mem {G : Type u_2} [Group G] [StarMul G] {g : G} (hg : g ∈ unitary G) :
g⁻¹ ∈ unitary G
source
def unitarySubgroup (G : Type u_2) [Group G] [StarMul G] :
Subgroup G

`unitary` as a `Subgroup` of a group.

Note the group structure on this type is not defeq to the one on `unitary`. This situation naturally arises when considering the unitary elements as a subgroup of the group of units of a star monoid.

Equations

- unitarySubgroup G = { toSubmonoid := unitary G, inv_mem' := ⋯ }

Instances For

source
@[simp]
theorem unitarySubgroup_toSubmonoid {G : Type u_2} [Group G] [StarMul G] :
(unitarySubgroup G).toSubmonoid = unitary G
source
@[simp]
theorem mem_unitarySubgroup_iff {G : Type u_2} [Group G] [StarMul G] {g : G} :
g ∈ unitarySubgroup G ↔ g ∈ unitary G
source
theorem Unitary.inv_mem_iff {G : Type u_2} [Group G] [StarMul G] {g : G} :
g⁻¹ ∈ unitary G ↔ g ∈ unitary G
source
theorem Unitary.smul_mem_of_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] {r : R} {a : A} (hr : r ∈ unitary R) (ha : a ∈ unitary A) :
r • a ∈ unitary A
source
theorem Unitary.smul_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) {a : A} (ha : a ∈ unitary A) :
r • a ∈ unitary A
source
instance Unitary.instSMulSubtypeMemSubmonoidUnitary {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :
SMul ↥(unitary R) ↥(unitary A)
Equations

- Unitary.instSMulSubtypeMemSubmonoidUnitary = { smul := fun (r : ↥(unitary R)) (a : ↥(unitary A)) => ⟨r • ↑a, ⋯⟩ }

source
@[simp]
theorem Unitary.coe_smul {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) (a : ↥(unitary A)) :
↑(r • a) = r • ↑a
source
instance Unitary.instMulActionSubtypeMemSubmonoidUnitary {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :
MulAction ↥(unitary R) ↥(unitary A)
Equations

- Unitary.instMulActionSubtypeMemSubmonoidUnitary = { toSMul := Unitary.instSMulSubtypeMemSubmonoidUnitary, one_smul := ⋯, mul_smul := ⋯ }

source
instance Unitary.instStarModuleSubtypeMemSubmonoidUnitary {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :
StarModule ↥(unitary R) ↥(unitary A)
source
instance Unitary.instSMulCommClassSubtypeMemSubmonoidUnitary {R : Type u_1} {S : Type u_2} {A : Type u_3} [Monoid R] [Monoid S] [Monoid A] [StarMul R] [StarMul S] [StarMul A] [MulAction R A] [MulAction S A] [StarModule R A] [StarModule S A] [IsScalarTower R A A] [IsScalarTower S A A] [SMulCommClass R A A] [SMulCommClass S A A] [SMulCommClass R S A] :
SMulCommClass ↥(unitary R) ↥(unitary S) ↥(unitary A)
source
instance Unitary.instIsScalarTowerSubtypeMemSubmonoidUnitary {R : Type u_1} {S : Type u_2} {A : Type u_3} [Monoid R] [Monoid S] [Monoid A] [StarMul R] [StarMul S] [StarMul A] [MulAction R S] [MulAction R A] [MulAction S A] [StarModule R S] [StarModule R A] [StarModule S A] [IsScalarTower R A A] [IsScalarTower S A A] [SMulCommClass R A A] [SMulCommClass S A A] [IsScalarTower R S S] [SMulCommClass R S S] [IsScalarTower R S A] :
IsScalarTower ↥(unitary R) ↥(unitary S) ↥(unitary A)
source
theorem Unitary.map_mem {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {F : Type u_5} [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R} (hr : r ∈ unitary R) :
f r ∈ unitary S
source
def Unitary.map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :
↥(unitary R) →⋆* ↥(unitary S)

The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of the underlying star monoids.

Equations

- Unitary.map f = { toFun := Subtype.map ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem Unitary.map_coe {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (a✝ : ↥(unitary R)) :
(map f) a✝ = Subtype.map ⇑f ⋯ a✝
source
@[simp]
theorem Unitary.coe_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :
↑((map f) x) = f ↑x
source
@[simp]
theorem Unitary.coe_map_star {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :
↑((map f) (star x)) = f (star ↑x)
source
@[simp]
theorem Unitary.map_id {R : Type u_2} [Monoid R] [StarMul R] :
map (StarMonoidHom.id R) = StarMonoidHom.id ↥(unitary R)
source
theorem Unitary.map_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (g : S →⋆* T) (f : R →⋆* S) :
map (g.comp f) = (map g).comp (map f)
source
@[simp]
theorem Unitary.map_injective {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {f : R →⋆* S} (hf : Function.Injective ⇑f) :
Function.Injective ⇑(map f)
source
theorem Unitary.toUnits_comp_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :
toUnits.comp (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits
source
def Unitary.mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
↥(unitary R) ≃⋆* ↥(unitary S)

The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of the underlying star monoids.

Equations

- Unitary.mapEquiv f = { toFun := ⇑(Unitary.map f.toStarMonoidHom), invFun := ⇑(Unitary.map f.symm.toStarMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem Unitary.mapEquiv_apply {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) (a : ↥(unitary R)) :
(mapEquiv f) a = (map f.toStarMonoidHom) a
source
@[simp]
theorem Unitary.mapEquiv_symm_apply {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) (a : ↥(unitary S)) :
(mapEquiv f).symm a = (map f.symm.toStarMonoidHom) a
source
@[simp]
theorem Unitary.mapEquiv_refl {R : Type u_2} [Monoid R] [StarMul R] :
mapEquiv (StarMulEquiv.refl R) = StarMulEquiv.refl ↥(unitary R)
source
@[simp]
theorem Unitary.mapEquiv_symm {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
mapEquiv f.symm = (mapEquiv f).symm
source
@[simp]
theorem Unitary.mapEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (f : R ≃⋆* S) (g : S ≃⋆* T) :
mapEquiv (f.trans g) = (mapEquiv f).trans (mapEquiv g)
source
@[simp]
theorem Unitary.toMonoidHom_mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
(mapEquiv f).toStarMonoidHom = map f.toStarMonoidHom
source
def unitarySubgroupUnitsEquiv {M : Type u_5} [Monoid M] [StarMul M] :
↥(unitarySubgroup M ˣ) ≃* ↥(unitary M)

The unitary subgroup of the units is equivalent to the unitary elements of the monoid.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe {M : Type u_5} [Monoid M] [StarMul M] (x : ↥(unitary M)) :
↑(↑(unitarySubgroupUnitsEquiv.symm x))⁻¹ = star ↑x
source
@[simp]
theorem unitarySubgroupUnitsEquiv_apply_coe {M : Type u_5} [Monoid M] [StarMul M] (x : ↥(unitarySubgroup M ˣ)) :
↑(unitarySubgroupUnitsEquiv x) = ↑↑x
source
@[simp]
theorem val_unitarySubgroupUnitsEquiv_symm_apply_coe {M : Type u_5} [Monoid M] [StarMul M] (x : ↥(unitary M)) :
↑↑(unitarySubgroupUnitsEquiv.symm x) = ↑x
source
instance Unitary.instCommGroupSubtypeMemSubmonoidUnitary {R : Type u_1} [CommMonoid R] [StarMul R] :
CommGroup ↥(unitary R)
Equations

- Unitary.instCommGroupSubtypeMemSubmonoidUnitary = { toGroup := inferInstanceAs (Group ↥(unitary R)), mul_comm := ⋯ }

source
theorem Unitary.mem_iff_star_mul_self {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :
U ∈ unitary R ↔ star U * U = 1
source
theorem Unitary.mem_iff_self_mul_star {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :
U ∈ unitary R ↔ U * star U = 1
source
theorem Unitary.coe_inv {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) :
↑U⁻¹ = (↑U)⁻¹
source
theorem Unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ U₂ : ↥(unitary R)) :
↑(U₁ / U₂) = ↑U₁ / ↑U₂
source
theorem Unitary.coe_zpow {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) (z : ℤ) :
↑(U ^ z) = ↑U ^ z
source
instance Unitary.instNegSubtypeMemSubmonoidUnitary {R : Type u_1} [Ring R] [StarRing R] :
Neg ↥(unitary R)
Equations

- Unitary.instNegSubtypeMemSubmonoidUnitary = { neg := fun (U : ↥(unitary R)) => ⟨-↑U, ⋯⟩ }

source
theorem Unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : ↥(unitary R)) :
↑(-U) = -↑U
source
instance Unitary.instHasDistribNegSubtypeMemSubmonoidUnitary {R : Type u_1} [Ring R] [StarRing R] :
HasDistribNeg ↥(unitary R)
Equations

- Unitary.instHasDistribNegSubtypeMemSubmonoidUnitary = Function.Injective.hasDistribNeg (fun (a : ↥(unitary R)) => ↑a) ⋯ ⋯ ⋯

source
@[simp]
theorem Unitary.spectrum_star_right_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} :
spectrum R (↑U * a * star ↑U) = spectrum R a

Unitary conjugation preserves the spectrum, star on right.

source
@[simp]
theorem Unitary.spectrum_star_left_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} :
spectrum R (star ↑U * a * ↑U) = spectrum R a

Unitary conjugation preserves the spectrum, star on left.

source
theorem IsStarProjection.two_mul_sub_one_mem_unitary {R : Type u_2} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :
2 * p - 1 ∈ unitary R

### Deprecated results #

source
@[deprecated Unitary.mem_iff (since := "2025-10-29")]
theorem unitary.mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :
U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1

Alias of `Unitary.mem_iff`.

source
@[deprecated Unitary.star_mul_self_of_mem (since := "2025-10-29")]
theorem unitary.star_mul_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :
star U * U = 1

Alias of `Unitary.star_mul_self_of_mem`.

source
@[deprecated Unitary.mul_star_self_of_mem (since := "2025-10-29")]
theorem unitary.mul_star_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :
U * star U = 1

Alias of `Unitary.mul_star_self_of_mem`.

source
@[deprecated Unitary.star_mem (since := "2025-10-29")]
theorem unitary.star_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :
star U ∈ unitary R

Alias of `Unitary.star_mem`.

source
@[deprecated Unitary.star_mem_iff (since := "2025-10-29")]
theorem unitary.star_mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :
star U ∈ unitary R ↔ U ∈ unitary R

Alias of `Unitary.star_mem_iff`.

source
@[deprecated Unitary.coe_star (since := "2025-10-29")]
theorem unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : ↥(unitary R)} :
↑(star U) = star ↑U

Alias of `Unitary.coe_star`.

source
@[deprecated Unitary.coe_star_mul_self (since := "2025-10-29")]
theorem unitary.coe_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
star ↑U * ↑U = 1

Alias of `Unitary.coe_star_mul_self`.

source
@[deprecated Unitary.coe_mul_star_self (since := "2025-10-29")]
theorem unitary.coe_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
↑U * ↑(star U) = 1

Alias of `Unitary.coe_mul_star_self`.

source
@[deprecated Unitary.star_mul_self (since := "2025-10-29")]
theorem unitary.star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
star U * U = 1

Alias of `Unitary.star_mul_self`.

source
@[deprecated Unitary.mul_star_self (since := "2025-10-29")]
theorem unitary.mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
U * star U = 1

Alias of `Unitary.mul_star_self`.

source
@[deprecated Unitary.star_eq_inv (since := "2025-10-29")]
theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
star U = U⁻¹

Alias of `Unitary.star_eq_inv`.

source
@[deprecated Unitary.star_eq_inv' (since := "2025-10-29")]
theorem unitary.star_eq_inv' {R : Type u_1} [Monoid R] [StarMul R] :
star = Inv.inv

Alias of `Unitary.star_eq_inv'`.

source
@[deprecated Unitary.toUnits (since := "2025-10-29")]
def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :
↥(unitary R) →* R ˣ

Alias of `Unitary.toUnits`.

The unitary elements embed into the units.

Equations

- @unitary.toUnits = @Unitary.toUnits

Instances For

source
@[deprecated Unitary.val_toUnits_apply (since := "2025-10-29")]
theorem unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :
↑(Unitary.toUnits x) = ↑x

Alias of `Unitary.val_toUnits_apply`.

source
@[deprecated Unitary.toUnits_injective (since := "2025-10-29")]
theorem unitary.toUnits_injective {R : Type u_1} [Monoid R] [StarMul R] :
Function.Injective ⇑Unitary.toUnits

Alias of `Unitary.toUnits_injective`.

source
@[deprecated Unitary.mul_left_inj (since := "2025-10-29")]
theorem unitary.mul_left_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :
x * ↑U = y * ↑U ↔ x = y

Alias of `Unitary.mul_left_inj`.

For unitary `U` in a star-monoid `R`, `x * U = y * U` if and only if `x = y` for all `x` and `y` in `R`.

source
@[deprecated Unitary.mul_right_inj (since := "2025-10-29")]
theorem unitary.mul_right_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :
↑U * x = ↑U * y ↔ x = y

Alias of `Unitary.mul_right_inj`.

For unitary `U` in a star-monoid `R`, `U * x = U * y` if and only if `x = y` for all `x` and `y` in `R`.

source
@[deprecated Unitary.mul_inv_mem_iff (since := "2025-10-29")]
theorem unitary.mul_inv_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b

Alias of `Unitary.mul_inv_mem_iff`.

source
@[deprecated Unitary.inv_mul_mem_iff (since := "2025-10-29")]
theorem unitary.inv_mul_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b

Alias of `Unitary.inv_mul_mem_iff`.

source
@[deprecated Unitary.inv_mem (since := "2025-10-29")]
theorem unitary.inv_mem {G : Type u_2} [Group G] [StarMul G] {g : G} (hg : g ∈ unitary G) :
g⁻¹ ∈ unitary G

Alias of `Unitary.inv_mem`.

source
@[deprecated Unitary.smul_mem_of_mem (since := "2025-10-29")]
theorem unitary.smul_mem_of_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] {r : R} {a : A} (hr : r ∈ unitary R) (ha : a ∈ unitary A) :
r • a ∈ unitary A

Alias of `Unitary.smul_mem_of_mem`.

source
@[deprecated Unitary.smul_mem (since := "2025-10-29")]
theorem unitary.smul_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) {a : A} (ha : a ∈ unitary A) :
r • a ∈ unitary A

Alias of `Unitary.smul_mem`.

source
@[deprecated Unitary.coe_smul (since := "2025-10-29")]
theorem unitary.coe_smul {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) (a : ↥(unitary A)) :
↑(r • a) = r • ↑a

Alias of `Unitary.coe_smul`.

source
@[deprecated Unitary.map_mem (since := "2025-10-29")]
theorem unitary.map_mem {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {F : Type u_5} [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R} (hr : r ∈ unitary R) :
f r ∈ unitary S

Alias of `Unitary.map_mem`.

source
@[deprecated Unitary.map (since := "2025-10-29")]
def unitary.map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :
↥(unitary R) →⋆* ↥(unitary S)

Alias of `Unitary.map`.

The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of the underlying star monoids.

Equations

- @unitary.map = @Unitary.map

Instances For

source
@[deprecated Unitary.coe_map (since := "2025-10-29")]
theorem unitary.coe_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :
↑((Unitary.map f) x) = f ↑x

Alias of `Unitary.coe_map`.

source
@[deprecated Unitary.coe_map_star (since := "2025-10-29")]
theorem unitary.coe_map_star {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :
↑((Unitary.map f) (star x)) = f (star ↑x)

Alias of `Unitary.coe_map_star`.

source
@[deprecated Unitary.map_id (since := "2025-10-29")]
theorem unitary.map_id {R : Type u_2} [Monoid R] [StarMul R] :
Unitary.map (StarMonoidHom.id R) = StarMonoidHom.id ↥(unitary R)

Alias of `Unitary.map_id`.

source
@[deprecated Unitary.map_comp (since := "2025-10-29")]
theorem unitary.map_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (g : S →⋆* T) (f : R →⋆* S) :
Unitary.map (g.comp f) = (Unitary.map g).comp (Unitary.map f)

Alias of `Unitary.map_comp`.

source
@[deprecated Unitary.map_injective (since := "2025-10-29")]
theorem unitary.map_injective {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {f : R →⋆* S} (hf : Function.Injective ⇑f) :
Function.Injective ⇑(Unitary.map f)

Alias of `Unitary.map_injective`.

source
@[deprecated Unitary.toUnits_comp_map (since := "2025-10-29")]
theorem unitary.toUnits_comp_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :
Unitary.toUnits.comp (Unitary.map f).toMonoidHom = (Units.map f.toMonoidHom).comp Unitary.toUnits

Alias of `Unitary.toUnits_comp_map`.

source
@[deprecated Unitary.mapEquiv (since := "2025-10-29")]
def unitary.mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
↥(unitary R) ≃⋆* ↥(unitary S)

Alias of `Unitary.mapEquiv`.

The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of the underlying star monoids.

Equations

- @unitary.mapEquiv = @Unitary.mapEquiv

Instances For

source
@[deprecated Unitary.mapEquiv_refl (since := "2025-10-29")]
theorem unitary.mapEquiv_refl {R : Type u_2} [Monoid R] [StarMul R] :
Unitary.mapEquiv (StarMulEquiv.refl R) = StarMulEquiv.refl ↥(unitary R)

Alias of `Unitary.mapEquiv_refl`.

source
@[deprecated Unitary.mapEquiv_symm (since := "2025-10-29")]
theorem unitary.mapEquiv_symm {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
Unitary.mapEquiv f.symm = (Unitary.mapEquiv f).symm

Alias of `Unitary.mapEquiv_symm`.

source
@[deprecated Unitary.mapEquiv_trans (since := "2025-10-29")]
theorem unitary.mapEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (f : R ≃⋆* S) (g : S ≃⋆* T) :
Unitary.mapEquiv (f.trans g) = (Unitary.mapEquiv f).trans (Unitary.mapEquiv g)

Alias of `Unitary.mapEquiv_trans`.

source
@[deprecated Unitary.toMonoidHom_mapEquiv (since := "2025-10-29")]
theorem unitary.toMonoidHom_mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
(Unitary.mapEquiv f).toStarMonoidHom = Unitary.map f.toStarMonoidHom

Alias of `Unitary.toMonoidHom_mapEquiv`.

source
@[deprecated Unitary.mem_iff_star_mul_self (since := "2025-10-29")]
theorem unitary.mem_iff_star_mul_self {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :
U ∈ unitary R ↔ star U * U = 1

Alias of `Unitary.mem_iff_star_mul_self`.

source
@[deprecated Unitary.mem_iff_self_mul_star (since := "2025-10-29")]
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :
U ∈ unitary R ↔ U * star U = 1

Alias of `Unitary.mem_iff_self_mul_star`.

source
@[deprecated Unitary.coe_inv (since := "2025-10-29")]
theorem unitary.coe_inv {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) :
↑U⁻¹ = (↑U)⁻¹

Alias of `Unitary.coe_inv`.

source
@[deprecated Unitary.coe_div (since := "2025-10-29")]
theorem unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ U₂ : ↥(unitary R)) :
↑(U₁ / U₂) = ↑U₁ / ↑U₂

Alias of `Unitary.coe_div`.

source
@[deprecated Unitary.coe_zpow (since := "2025-10-29")]
theorem unitary.coe_zpow {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) (z : ℤ) :
↑(U ^ z) = ↑U ^ z

Alias of `Unitary.coe_zpow`.

source
@[deprecated Unitary.coe_neg (since := "2025-10-29")]
theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : ↥(unitary R)) :
↑(-U) = -↑U

Alias of `Unitary.coe_neg`.

source
@[deprecated Unitary.spectrum_star_right_conjugate (since := "2025-10-20")]
theorem unitary.spectrum.unitary_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} :
spectrum R (↑U * a * star ↑U) = spectrum R a

Alias of `Unitary.spectrum_star_right_conjugate`.

Unitary conjugation preserves the spectrum, star on right.

source
@[deprecated Unitary.spectrum_star_left_conjugate (since := "2025-10-20")]
theorem unitary.spectrum.unitary_conjugate' {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} :
spectrum R (star ↑U * a * ↑U) = spectrum R a

Alias of `Unitary.spectrum_star_left_conjugate`.

Unitary conjugation preserves the spectrum, star on left.