[GOAL]
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ ball 0 1
hy : b✝ ∈ ball 0 1
⊢ a✝ * b✝ ∈ ball 0 1
[PROOFSTEP]
rw [mem_ball_zero_iff] at *
[GOAL]
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ < 1
hy : ‖b✝‖ < 1
⊢ ‖a✝ * b✝‖ < 1
[PROOFSTEP]
exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)
[GOAL]
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ closedBall 0 1
hy : b✝ ∈ closedBall 0 1
⊢ a✝ * b✝ ∈ closedBall 0 1
[PROOFSTEP]
rw [mem_closedBall_zero_iff] at *
[GOAL]
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ ≤ 1
hy : ‖b✝‖ ≤ 1
⊢ ‖a✝ * b✝‖ ≤ 1
[PROOFSTEP]
exact (norm_mul_le _ _).trans (mul_le_one hx (norm_nonneg _) hy)
[GOAL]
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NormedDivisionRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ sphere 0 1
hy : b✝ ∈ sphere 0 1
⊢ a✝ * b✝ ∈ sphere 0 1
[PROOFSTEP]
rw [mem_sphere_zero_iff_norm] at *
[GOAL]
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NormedDivisionRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ = 1
hy : ‖b✝‖ = 1
⊢ ‖a✝ * b✝‖ = 1
[PROOFSTEP]
simp [*]
[GOAL]
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
⊢ ‖(↑x)⁻¹‖ = 1
[PROOFSTEP]
rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]
[GOAL]
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ ‖↑x / ↑y‖ = 1
[PROOFSTEP]
rw [norm_div, mem_sphere_zero_iff_norm.1 x.coe_prop, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]
[GOAL]
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
n : ℤ
⊢ ↑x ^ n ∈ sphere 0 1
[PROOFSTEP]
rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]
[GOAL]
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
h : ↑(unitSphereToUnits 𝕜) x = ↑(unitSphereToUnits 𝕜) y
⊢ ↑x = ↑y
[PROOFSTEP]
convert congr_arg Units.val h
