chore: move results from unitary namespace to Unitary (#30697)

All results living in the `unitary` namespace is now in the `Unitary` namespace.

And the results `unitary.spectrum.unitary_conjugate` and `unitary.spectrum.unitary_conjugate'` are renamed to `Unitary.spectrum_star_conjugate_left` and `Unitary.spectrum_star_conjugate_right` to match the renaming convention in #30692.

Author: themathqueen

Mathlib/Algebra/Star/Unitary.lean

@@ -44,7 +44,7 @@ def unitary (R : Type*) [Monoid R] [StarMul R] : Submonoid R where
 
 variable {R : Type*}
 
-namespace unitary
+namespace Unitary
 
 section Monoid
 
@@ -127,7 +127,7 @@ theorem toUnits_injective : Function.Injective (toUnits : unitary R → Rˣ) :=
 
 theorem _root_.IsUnit.mem_unitary_iff_star_mul_self {u : R} (hu : IsUnit u) :
     u ∈ unitary R ↔ star u * u = 1 := by
-  rw [unitary.mem_iff, and_iff_left_of_imp fun h_mul => ?_]
+  rw [mem_iff, and_iff_left_of_imp fun h_mul => ?_]
   lift u to Rˣ using hu
   exact left_inv_eq_right_inv h_mul u.mul_inv ▸ u.mul_inv
 
@@ -142,13 +142,13 @@ alias ⟨_, _root_.IsUnit.mem_unitary_of_mul_star_self⟩ := IsUnit.mem_unitary_
 for all `x` and `y` in `R`. -/
 protected theorem mul_left_inj {x y : R} (U : unitary R) :
     x * U = y * U ↔ x = y :=
-  unitary.val_toUnits_apply U ▸ Units.mul_left_inj _
+  val_toUnits_apply U ▸ Units.mul_left_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`. -/
 protected theorem mul_right_inj {x y : R} (U : unitary R) :
     U * x = U * y ↔ x = y :=
-  unitary.val_toUnits_apply U ▸ Units.mul_right_inj _
+  val_toUnits_apply U ▸ Units.mul_right_inj _
 
 lemma mul_inv_mem_iff {G : Type*} [Group G] [StarMul G] (a b : G) :
     a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b := by
@@ -161,7 +161,7 @@ lemma inv_mul_mem_iff {G : Type*} [Group G] [StarMul G] (a b : G) :
 
 theorem _root_.Units.unitary_eq : unitary Rˣ = (unitary R).comap (Units.coeHom R) := by
   ext
-  simp [unitary.mem_iff, Units.ext_iff]
+  simp [mem_iff, Units.ext_iff]
 
 /-- In a star monoid, the product `a * b⁻¹` of units is unitary if `star a * a = star b * b`. -/
 protected lemma _root_.Units.mul_inv_mem_unitary (a b : Rˣ) :
@@ -185,14 +185,14 @@ lemma _root_.isStarNormal_of_mem_unitary {u : R} (hu : u ∈ unitary R) : IsStar
 
 end Monoid
 
-end unitary
+end Unitary
 
 section Group
 
 variable {G : Type*} [Group G] [StarMul G]
 
-theorem unitary.inv_mem {g : G} (hg : g ∈ unitary G) : g⁻¹ ∈ unitary G := by
-  simp_rw [unitary.mem_iff, star_inv, ← mul_inv_rev, inv_eq_one] at *
+theorem Unitary.inv_mem {g : G} (hg : g ∈ unitary G) : g⁻¹ ∈ unitary G := by
+  simp_rw [mem_iff, star_inv, ← mul_inv_rev, inv_eq_one] at *
   exact hg.symm
 
 variable (G) in
@@ -203,7 +203,7 @@ This situation naturally arises when considering the unitary elements as a
 subgroup of the group of units of a star monoid. -/
 def unitarySubgroup : Subgroup G where
   toSubmonoid := unitary G
-  inv_mem' := unitary.inv_mem
+  inv_mem' := Unitary.inv_mem
 
 @[simp]
 theorem unitarySubgroup_toSubmonoid : (unitarySubgroup G).toSubmonoid = unitary G := rfl
@@ -212,12 +212,12 @@ theorem unitarySubgroup_toSubmonoid : (unitarySubgroup G).toSubmonoid = unitary
 theorem mem_unitarySubgroup_iff {g : G} : g ∈ unitarySubgroup G ↔ g ∈ unitary G :=
   Iff.rfl
 
-nonrec theorem unitary.inv_mem_iff {g : G} : g⁻¹ ∈ unitary G ↔ g ∈ unitary G :=
+nonrec theorem Unitary.inv_mem_iff {g : G} : g⁻¹ ∈ unitary G ↔ g ∈ unitary G :=
   inv_mem_iff (H := unitarySubgroup G)
 
 end Group
 
-namespace unitary
+namespace Unitary
 
 section SMul
 
@@ -276,7 +276,7 @@ variable {R S T : Type*} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T
 
 lemma map_mem {F : Type*} [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S]
     (f : F) {r : R} (hr : r ∈ unitary R) : f r ∈ unitary S := by
-  rw [unitary.mem_iff] at hr
+  rw [mem_iff] at hr
   simpa [map_star, map_mul] using And.intro congr(f $(hr.1)) congr(f $(hr.2))
 
 /-- The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of
@@ -404,25 +404,78 @@ universe u
 
 variable {R A : Type*} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A]
 
-/-- Unitary conjugation preserves the spectrum, star on left. -/
+/-- Unitary conjugation preserves the spectrum, star on right. -/
 @[simp]
-lemma spectrum.unitary_conjugate {a : A} {u : unitary A} :
-    spectrum R (u * a * (star u : A)) = spectrum R a :=
-  spectrum.units_conjugate (u := unitary.toUnits u)
+lemma spectrum_star_right_conjugate {a : A} {U : unitary A} :
+    spectrum R (U * a * (star U : A)) = spectrum R a :=
+  spectrum.units_conjugate (u := toUnits U)
 
-/-- Unitary conjugation preserves the spectrum, star on right. -/
+/-- Unitary conjugation preserves the spectrum, star on left. -/
 @[simp]
-lemma spectrum.unitary_conjugate' {a : A} {u : unitary A} :
-    spectrum R ((star u : A) * a * u) = spectrum R a := by
-  simpa using spectrum.unitary_conjugate (u := star u)
+lemma spectrum_star_left_conjugate {a : A} {U : unitary A} :
+    spectrum R ((star U : A) * a * U) = spectrum R a := by
+  simpa using spectrum_star_right_conjugate (U := star U)
 
 end UnitaryConjugate
 
-end unitary
+end Unitary
 
 theorem IsStarProjection.two_mul_sub_one_mem_unitary {R : Type*} [Ring R] [StarRing R] {p : R}
     (hp : IsStarProjection p) : 2 * p - 1 ∈ unitary R := by
-  simp only [two_mul, unitary.mem_iff, star_sub, star_add,
+  simp only [two_mul, Unitary.mem_iff, star_sub, star_add,
     hp.isSelfAdjoint.star_eq, star_one, mul_sub, mul_add,
     sub_mul, add_mul, hp.isIdempotentElem.eq, one_mul, add_sub_cancel_right,
     mul_one, sub_sub_cancel, and_self]
+
+namespace unitary
+
+/-! ### Deprecated results -/
+
+@[deprecated (since := "2025-10-29")] alias mem_iff := Unitary.mem_iff
+@[deprecated (since := "2025-10-29")] alias star_mul_self_of_mem := Unitary.star_mul_self_of_mem
+@[deprecated (since := "2025-10-29")] alias mul_star_self_of_mem := Unitary.mul_star_self_of_mem
+@[deprecated (since := "2025-10-29")] alias star_mem := Unitary.star_mem
+@[deprecated (since := "2025-10-29")] alias star_mem_iff := Unitary.star_mem_iff
+@[deprecated (since := "2025-10-29")] alias coe_star := Unitary.coe_star
+@[deprecated (since := "2025-10-29")] alias coe_star_mul_self := Unitary.coe_star_mul_self
+@[deprecated (since := "2025-10-29")] alias coe_mul_star_self := Unitary.coe_mul_star_self
+@[deprecated (since := "2025-10-29")] alias star_mul_self := Unitary.star_mul_self
+@[deprecated (since := "2025-10-29")] alias mul_star_self := Unitary.mul_star_self
+@[deprecated (since := "2025-10-29")] alias star_eq_inv := Unitary.star_eq_inv
+@[deprecated (since := "2025-10-29")] alias star_eq_inv' := Unitary.star_eq_inv'
+@[deprecated (since := "2025-10-29")] alias toUnits := Unitary.toUnits
+@[deprecated (since := "2025-10-29")] alias val_toUnits_apply := Unitary.val_toUnits_apply
+@[deprecated (since := "2025-10-29")] alias toUnits_injective := Unitary.toUnits_injective
+@[deprecated (since := "2025-10-29")] alias mul_left_inj := Unitary.mul_left_inj
+@[deprecated (since := "2025-10-29")] alias mul_right_inj := Unitary.mul_right_inj
+@[deprecated (since := "2025-10-29")] alias mul_inv_mem_iff := Unitary.mul_inv_mem_iff
+@[deprecated (since := "2025-10-29")] alias inv_mul_mem_iff := Unitary.inv_mul_mem_iff
+@[deprecated (since := "2025-10-29")] alias inv_mem := Unitary.inv_mem
+@[deprecated (since := "2025-10-29")] alias smul_mem_of_mem := Unitary.smul_mem_of_mem
+@[deprecated (since := "2025-10-29")] alias smul_mem := Unitary.smul_mem
+@[deprecated (since := "2025-10-29")] alias coe_smul := Unitary.coe_smul
+@[deprecated (since := "2025-10-29")] alias map_mem := Unitary.map_mem
+@[deprecated (since := "2025-10-29")] alias map := Unitary.map
+@[deprecated (since := "2025-10-29")] alias coe_map := Unitary.coe_map
+@[deprecated (since := "2025-10-29")] alias coe_map_star := Unitary.coe_map_star
+@[deprecated (since := "2025-10-29")] alias map_id := Unitary.map_id
+@[deprecated (since := "2025-10-29")] alias map_comp := Unitary.map_comp
+@[deprecated (since := "2025-10-29")] alias map_injective := Unitary.map_injective
+@[deprecated (since := "2025-10-29")] alias toUnits_comp_map := Unitary.toUnits_comp_map
+@[deprecated (since := "2025-10-29")] alias mapEquiv := Unitary.mapEquiv
+@[deprecated (since := "2025-10-29")] alias mapEquiv_refl := Unitary.mapEquiv_refl
+@[deprecated (since := "2025-10-29")] alias mapEquiv_symm := Unitary.mapEquiv_symm
+@[deprecated (since := "2025-10-29")] alias mapEquiv_trans := Unitary.mapEquiv_trans
+@[deprecated (since := "2025-10-29")] alias toMonoidHom_mapEquiv := Unitary.toMonoidHom_mapEquiv
+@[deprecated (since := "2025-10-29")] alias mem_iff_star_mul_self := Unitary.mem_iff_star_mul_self
+@[deprecated (since := "2025-10-29")] alias mem_iff_self_mul_star := Unitary.mem_iff_self_mul_star
+@[deprecated (since := "2025-10-29")] alias coe_inv := Unitary.coe_inv
+@[deprecated (since := "2025-10-29")] alias coe_div := Unitary.coe_div
+@[deprecated (since := "2025-10-29")] alias coe_zpow := Unitary.coe_zpow
+@[deprecated (since := "2025-10-29")] alias coe_neg := Unitary.coe_neg
+@[deprecated (since := "2025-10-20")] alias spectrum.unitary_conjugate :=
+  Unitary.spectrum_star_right_conjugate
+@[deprecated (since := "2025-10-20")] alias spectrum.unitary_conjugate' :=
+  Unitary.spectrum_star_left_conjugate
+
+end unitary

Mathlib/Analysis/CStarAlgebra/Basic.lean

@@ -212,7 +212,7 @@ instance (priority := 100) [Nontrivial E] : NormOneClass E :=
 
 theorem norm_coe_unitary [Nontrivial E] (U : unitary E) : ‖(U : E)‖ = 1 := by
   rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
-    unitary.coe_star_mul_self, CStarRing.norm_one]
+    Unitary.coe_star_mul_self, CStarRing.norm_one]
 
 @[simp]
 theorem norm_of_mem_unitary [Nontrivial E] {U : E} (hU : U ∈ unitary E) : ‖U‖ = 1 :=
@@ -226,7 +226,7 @@ theorem norm_coe_unitary_mul (U : unitary E) (A : E) : ‖(U : E) * A‖ = ‖A
       _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
       _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]
   · calc
-      _ = ‖(U : E)⋆ * U * A‖ := by rw [unitary.coe_star_mul_self U, one_mul]
+      _ = ‖(U : E)⋆ * U * A‖ := by rw [Unitary.coe_star_mul_self U, one_mul]
       _ ≤ ‖(U : E)⋆‖ * ‖(U : E) * A‖ := by
         rw [mul_assoc]
         exact norm_mul_le _ _
@@ -244,7 +244,7 @@ theorem norm_mul_coe_unitary (A : E) (U : unitary E) : ‖A * U‖ = ‖A‖ :=
   calc
     _ = ‖((U : E)⋆ * A⋆)⋆‖ := by simp only [star_star, star_mul]
     _ = ‖(U : E)⋆ * A⋆‖ := by rw [norm_star]
-    _ = ‖A⋆‖ := norm_mem_unitary_mul (star A) (unitary.star_mem U.prop)
+    _ = ‖A⋆‖ := norm_mem_unitary_mul (star A) (Unitary.star_mem U.prop)
     _ = ‖A‖ := norm_star _
 
 theorem norm_mul_mem_unitary (A : E) {U : E} (hU : U ∈ unitary E) : ‖A * U‖ = ‖A‖ :=

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean

@@ -43,7 +43,7 @@ lemma unitary_iff_isStarNormal_and_spectrum_subset_unitary {u : A} :
   refine and_congr_right fun hu ↦ ?_
   nth_rw 1 [← cfc_id ℂ u]
   rw [cfc_unitary_iff id u, Set.subset_def]
-  simp only [id_eq, RCLike.star_def, SetLike.mem_coe, unitary.mem_iff_star_mul_self]
+  simp only [id_eq, RCLike.star_def, SetLike.mem_coe, Unitary.mem_iff_star_mul_self]
 
 lemma mem_unitary_of_spectrum_subset_unitary {u : A}
     [IsStarNormal u] (hu : spectrum ℂ u ⊆ unitary ℂ) : u ∈ unitary A :=

Mathlib/Analysis/CStarAlgebra/Matrix.lean

@@ -68,7 +68,7 @@ theorem entry_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Matrix.uni
     rw [diag_eq_norm_sum.1]
     norm_cast
   -- Since U is unitary, the diagonal entries of U * Uᴴ are all 1
-  have mul_eq_one : U * Uᴴ = 1 := unitary.mul_star_self_of_mem hU
+  have mul_eq_one : U * Uᴴ = 1 := Unitary.mul_star_self_of_mem hU
   have diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1 := by
     simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]
   -- Putting it all together

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -34,7 +34,7 @@ we can still establish a form of spectral permanence.
 
 ## Main statements
 
-+ `unitary.spectrum_subset_circle`: The spectrum of a unitary element is contained in the unit
++ `Unitary.spectrum_subset_circle`: The spectrum of a unitary element is contained in the unit
   sphere in `ℂ`.
 + `IsSelfAdjoint.spectralRadius_eq_nnnorm`: The spectral radius of a selfadjoint element is equal
   to its norm.
@@ -68,21 +68,24 @@ section UnitarySpectrum
 variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*} [NormedRing E] [StarRing E] [CStarRing E]
   [NormedAlgebra 𝕜 E] [CompleteSpace E]
 
-theorem unitary.spectrum_subset_circle (u : unitary E) :
+theorem Unitary.spectrum_subset_circle (u : unitary E) :
     spectrum 𝕜 (u : E) ⊆ Metric.sphere 0 1 := by
   nontriviality E
   refine fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm ?_ ?_)
   · simpa only [CStarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk
-  · rw [← unitary.val_toUnits_apply u] at hk
+  · rw [← Unitary.val_toUnits_apply u] at hk
     have hnk := ne_zero_of_mem_of_unit hk
-    rw [← inv_inv (unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk
-    have : ‖k‖⁻¹ ≤ ‖(↑(unitary.toUnits u)⁻¹ : E)‖ := by
+    rw [← inv_inv (Unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk
+    have : ‖k‖⁻¹ ≤ ‖(↑(Unitary.toUnits u)⁻¹ : E)‖ := by
       simpa only [norm_inv] using norm_le_norm_of_mem hk
     simpa using inv_le_of_inv_le₀ (norm_pos_iff.mpr hnk) this
 
+@[deprecated (since := "2025-10-29")] alias unitary.spectrum_subset_circle :=
+  Unitary.spectrum_subset_circle
+
 theorem spectrum.subset_circle_of_unitary {u : E} (h : u ∈ unitary E) :
     spectrum 𝕜 u ⊆ Metric.sphere 0 1 :=
-  unitary.spectrum_subset_circle ⟨u, h⟩
+  Unitary.spectrum_subset_circle ⟨u, h⟩
 
 theorem spectrum.norm_eq_one_of_unitary {u : E} (hu : u ∈ unitary E)
     ⦃z : 𝕜⦄ (hz : z ∈ spectrum 𝕜 u) : ‖z‖ = 1 := by