feat: add IsUnit.mem_unitary_of_star_mul_self and protect some `.st…

…ar` lemmas (#10855)
leanprover-community · Mar 1, 2024 · ec83de2 · ec83de2
1 parent 09884ec
commit ec83de2
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
@@ -559,7 +559,7 @@ instance {A : Type*} [Star A] [SMul R A] [StarModule R A] : StarModule Rˣ A :=
 
 end Units
 
-theorem IsUnit.star [Monoid R] [StarMul R] {a : R} : IsUnit a → IsUnit (star a)
+protected theorem IsUnit.star [Monoid R] [StarMul R] {a : R} : IsUnit a → IsUnit (star a)
   | ⟨u, hu⟩ => ⟨Star.star u, hu ▸ rfl⟩
 #align is_unit.star IsUnit.star
 
@@ -576,7 +576,7 @@ theorem Ring.inverse_star [Semiring R] [StarRing R] (a : R) :
   rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
 #align ring.inverse_star Ring.inverse_star
 
-instance Invertible.star {R : Type*} [MulOneClass R] [StarMul R] (r : R) [Invertible r] :
+protected instance Invertible.star {R : Type*} [MulOneClass R] [StarMul R] (r : R) [Invertible r] :
     Invertible (star r) where
   invOf := Star.star (⅟ r)
   invOf_mul_self := by rw [← star_mul, mul_invOf_self, star_one]

diff --git a/Mathlib/Algebra/Star/Unitary.lean b/Mathlib/Algebra/Star/Unitary.lean
@@ -139,6 +139,17 @@ theorem toUnits_injective : Function.Injective (toUnits : unitary R → Rˣ) :=
   Subtype.ext <| Units.ext_iff.mp h
 #align unitary.to_units_injective unitary.toUnits_injective
 
+theorem _root_.IsUnit.mem_unitary_of_star_mul_self  {u : R} (hu : IsUnit u)
+    (h_mul : star u * u = 1) : u ∈ unitary R := by
+  refine unitary.mem_iff.mpr ⟨h_mul, ?_⟩
+  lift u to Rˣ using hu
+  exact left_inv_eq_right_inv h_mul u.mul_inv ▸ u.mul_inv
+
+theorem _root_.IsUnit.mem_unitary_of_mul_star_self {u : R} (hu : IsUnit u)
+    (h_mul : u * star u = 1) : u ∈ unitary R :=
+  star_star u ▸
+    (hu.star.mem_unitary_of_star_mul_self ((star_star u).symm ▸ h_mul) |> unitary.star_mem)
+
 instance instIsStarNormal (u : unitary R) : IsStarNormal u where
   star_comm_self := star_mul_self u |>.trans <| (mul_star_self u).symm