feat(algebra/star/basic + analysis/normed_space/star/basic): add two …

…eq_zero/ne_zero lemmas (#12412)

Added two lemmas about elements being zero or non-zero.

Golf a proof.

src/algebra/star/basic.lean

@@ -146,7 +146,7 @@ op_injective $
   ((star_mul_equiv : R ≃* Rᵐᵒᵖ).to_monoid_hom.map_zpow x z).trans (op_zpow (star x) z).symm
 
 /-- When multiplication is commutative, `star` preserves division. -/
-@[simp] lemma star_div [comm_group R] [star_semigroup R] (x y : R) : 
+@[simp] lemma star_div [comm_group R] [star_semigroup R] (x y : R) :
   star (x / y) = star x / star y :=
 (star_mul_aut : R ≃* R).to_monoid_hom.map_div _ _
 
@@ -203,6 +203,13 @@ variables (R)
 
 variables {R}
 
+@[simp]
+lemma star_eq_zero [add_monoid R] [star_add_monoid R] {x : R} : star x = 0 ↔ x = 0 :=
+star_add_equiv.map_eq_zero_iff
+
+lemma star_ne_zero [add_monoid R] [star_add_monoid R] {x : R} : star x ≠ 0 ↔ x ≠ 0 :=
+star_eq_zero.not
+
 @[simp] lemma star_neg [add_group R] [star_add_monoid R] (r : R) : star (-r) = - star r :=
 (star_add_equiv : R ≃+ R).map_neg _
 

src/analysis/normed_space/star/basic.lean

@@ -108,20 +108,14 @@ variables [normed_ring E] [star_ring E] [cstar_ring E]
 /-- In a C*-ring, star preserves the norm. -/
 @[priority 100] -- see Note [lower instance priority]
 instance to_normed_star_monoid : normed_star_monoid E :=
-⟨begin
-  intro x,
-  by_cases htriv : x = 0,
-  { simp only [htriv, star_zero] },
-  { have hnt : 0 < ∥x∥ := norm_pos_iff.mpr htriv,
-    have hnt_star : 0 < ∥x⋆∥ :=
-      norm_pos_iff.mpr ((add_equiv.map_ne_zero_iff star_add_equiv).mpr htriv),
-    have h₁ := calc
-      ∥x∥ * ∥x∥ = ∥x⋆ * x∥        : norm_star_mul_self.symm
-            ... ≤ ∥x⋆∥ * ∥x∥      : norm_mul_le _ _,
-    have h₂ := calc
-      ∥x⋆∥ * ∥x⋆∥ = ∥x * x⋆∥      : by rw [←norm_star_mul_self, star_star]
-             ... ≤ ∥x∥ * ∥x⋆∥     : norm_mul_le _ _,
-    exact le_antisymm (le_of_mul_le_mul_right h₂ hnt_star) (le_of_mul_le_mul_right h₁ hnt) },
+⟨λ x, begin
+  have n_le : ∀ {y : E}, ∥y∥ ≤ ∥y⋆∥,
+  { intros y,
+    by_cases y0 : y = 0,
+    { rw [y0, star_zero] },
+    { refine le_of_mul_le_mul_right _ (norm_pos_iff.mpr y0),
+      exact (norm_star_mul_self.symm.trans_le $ norm_mul_le _ _) } },
+  exact (n_le.trans_eq $ congr_arg _ $ star_star _).antisymm n_le,
 end⟩
 
 lemma norm_self_mul_star {x : E} : ∥x * x⋆∥ = ∥x∥ * ∥x∥ :=