feat: unitary elements are normal (#10778)

leanprover-community · Feb 21, 2024 · c63ddc2 · c63ddc2
1 parent 88a36ee
commit c63ddc2
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 3 deletions.
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -596,6 +596,11 @@ protected instance IsStarNormal.neg [Ring R] [StarAddMonoid R] {x : R} [IsStarNo
     IsStarNormal (-x) :=
   ⟨show star (-x) * -x = -x * star (-x) by simp_rw [star_neg, neg_mul_neg, star_comm_self']⟩
 
+protected instance IsStarNormal.map {F R S : Type*} [Mul R] [Star R] [Mul S] [Star S]
+    [FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] :
+    IsStarNormal (f r) where
+  star_comm_self := by simpa [map_star] using congr(f $(hr.star_comm_self))
+
 -- see Note [lower instance priority]
 instance (priority := 100) TrivialStar.isStarNormal [Mul R] [StarMul R] [TrivialStar R]
     {x : R} : IsStarNormal x :=

diff --git a/Mathlib/Algebra/Star/Unitary.lean b/Mathlib/Algebra/Star/Unitary.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Frédéric Dupuis
 -/
-import Mathlib.Algebra.Star.Basic
+import Mathlib.Algebra.Star.SelfAdjoint
 import Mathlib.GroupTheory.Submonoid.Operations
 
 #align_import algebra.star.unitary from "leanprover-community/mathlib"@"247a102b14f3cebfee126293341af5f6bed00237"
@@ -135,9 +135,18 @@ def toUnits : unitary R →* Rˣ
   map_mul' _ _ := Units.ext rfl
 #align unitary.to_units unitary.toUnits
 
-theorem to_units_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h =>
+theorem toUnits_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h =>
   Subtype.ext <| Units.ext_iff.mp h
-#align unitary.to_units_injective unitary.to_units_injective
+#align unitary.to_units_injective unitary.toUnits_injective
+
+instance instIsStarNormal (u : unitary R) : IsStarNormal u where
+  star_comm_self := star_mul_self u |>.trans <| (mul_star_self u).symm
+
+instance coe_isStarNormal (u : unitary R) : IsStarNormal (u : R) where
+  star_comm_self := congr(Subtype.val $(star_comm_self' u))
+
+lemma _root_.isStarNormal_of_mem_unitary {u : R} (hu : u ∈ unitary R) : IsStarNormal u :=
+  coe_isStarNormal ⟨u, hu⟩
 
 end Monoid