# mathlib3documentation

analysis.normed.field.unit_ball

# Algebraic structures on unit balls and spheres #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define algebraic structures (semigroup, comm_semigroup, monoid, comm_monoid, group, comm_group) on metric.ball (0 : 𝕜) 1, metric.closed_ball (0 : 𝕜) 1, and metric.sphere (0 : 𝕜) 1. In each case we use the weakest possible typeclass assumption on 𝕜, from non_unital_semi_normed_ring to normed_field.

def subsemigroup.unit_ball (𝕜 : Type u_1)  :

Unit ball in a non unital semi normed ring as a bundled subsemigroup.

Equations
@[protected, instance]
def metric.ball.semigroup {𝕜 : Type u_1}  :
Equations
@[protected, instance]
def metric.ball.has_continuous_mul {𝕜 : Type u_1}  :
@[protected, instance]
def metric.ball.comm_semigroup {𝕜 : Type u_1}  :
Equations
@[protected, instance]
def metric.ball.has_distrib_neg {𝕜 : Type u_1}  :
Equations
• metric.ball.has_distrib_neg = metric.ball.has_distrib_neg._proof_1 metric.ball.has_distrib_neg._proof_2 metric.ball.has_distrib_neg._proof_3
@[simp, norm_cast]
theorem coe_mul_unit_ball {𝕜 : Type u_1} (x y : 1)) :
(x * y) = x * y
def subsemigroup.unit_closed_ball (𝕜 : Type u_1)  :

Closed unit ball in a non unital semi normed ring as a bundled subsemigroup.

Equations
@[protected, instance]
def metric.closed_ball.semigroup {𝕜 : Type u_1}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp, norm_cast]
theorem coe_mul_unit_closed_ball {𝕜 : Type u_1} (x y : 1)) :
(x * y) = x * y
def submonoid.unit_closed_ball (𝕜 : Type u_1)  :

Closed unit ball in a semi normed ring as a bundled submonoid.

Equations
@[protected, instance]
def metric.closed_ball.monoid {𝕜 : Type u_1}  :
Equations
@[protected, instance]
def metric.closed_ball.comm_monoid {𝕜 : Type u_1}  :
Equations
@[simp, norm_cast]
theorem coe_one_unit_closed_ball {𝕜 : Type u_1}  :
1 = 1
@[simp, norm_cast]
theorem coe_pow_unit_closed_ball {𝕜 : Type u_1} (x : 1)) (n : ) :
(x ^ n) = x ^ n
def submonoid.unit_sphere (𝕜 : Type u_1)  :

Unit sphere in a normed division ring as a bundled submonoid.

Equations
@[protected, instance]
def metric.sphere.has_inv {𝕜 : Type u_1}  :
Equations
@[simp, norm_cast]
theorem coe_inv_unit_sphere {𝕜 : Type u_1} (x : 1)) :
@[protected, instance]
def metric.sphere.has_div {𝕜 : Type u_1}  :
Equations
@[simp, norm_cast]
theorem coe_div_unit_sphere {𝕜 : Type u_1} (x y : 1)) :
(x / y) = x / y
@[protected, instance]
def int.has_pow {𝕜 : Type u_1}  :
Equations
@[simp, norm_cast]
theorem coe_zpow_unit_sphere {𝕜 : Type u_1} (x : 1)) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def metric.sphere.monoid {𝕜 : Type u_1}  :
Equations
@[simp, norm_cast]
theorem coe_one_unit_sphere {𝕜 : Type u_1}  :
1 = 1
@[simp, norm_cast]
theorem coe_mul_unit_sphere {𝕜 : Type u_1} (x y : 1)) :
(x * y) = x * y
@[simp, norm_cast]
theorem coe_pow_unit_sphere {𝕜 : Type u_1} (x : 1)) (n : ) :
(x ^ n) = x ^ n
def unit_sphere_to_units (𝕜 : Type u_1)  :
1) →* 𝕜ˣ

Monoid homomorphism from the unit sphere to the group of units.

Equations
• = (λ (x : 1)), _) _
@[simp]
theorem unit_sphere_to_units_apply_coe {𝕜 : Type u_1} (x : 1)) :
x) = x
theorem unit_sphere_to_units_injective {𝕜 : Type u_1}  :
@[protected, instance]
def metric.sphere.group {𝕜 : Type u_1}  :
Equations
• metric.sphere.group = metric.sphere.group._proof_1 metric.sphere.group._proof_2 metric.sphere.group._proof_3 metric.sphere.group._proof_4 metric.sphere.group._proof_5 metric.sphere.group._proof_6
@[protected, instance]
def metric.sphere.has_distrib_neg {𝕜 : Type u_1}  :
Equations
• metric.sphere.has_distrib_neg = metric.sphere.has_distrib_neg._proof_1 metric.sphere.has_distrib_neg._proof_2 metric.sphere.has_distrib_neg._proof_3
@[protected, instance]
def metric.sphere.topological_group {𝕜 : Type u_1}  :
@[protected, instance]
def metric.sphere.comm_group {𝕜 : Type u_1} [normed_field 𝕜] :
Equations