𝕜 : Type ?u.69584
E : Type u_1
α : Type ?u.69590
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1
𝕜 : Type ?u.69584
E : Type u_1
α : Type ?u.69590
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
no goals
𝕜 : Type ?u.69584
E : Type u_1
α : Type ?u.69590
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1
rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]