Commit 2022-06-25 20:02 f9571f0f

View on Github →

feat(analysis/normed*): add instances about balls and spheres (#14808) Non-bc change: has_inv.inv on the unit circle is now defined using has_inv.inv instead of complex conjugation.

Estimated changes

Modified src/analysis/complex/circle.lean

added def circle.of_conj_div_self

modified def circle.to_units

modified def circle

modified theorem coe_inv_circle

modified theorem coe_inv_circle_eq_conj

Created src/analysis/normed/field/unit_ball.lean

added def submonoid.unit_closed_ball

added def submonoid.unit_sphere

added def subsemigroup.unit_ball

added def subsemigroup.unit_closed_ball

added def unit_sphere_to_units

Created src/analysis/normed/group/ball_sphere.lean

added theorem coe_neg_ball

added theorem coe_neg_closed_ball

added theorem coe_neg_sphere

Modified src/analysis/normed/group/basic.lean

deleted theorem coe_neg_sphere

Created src/analysis/normed_space/ball_action.lean

added theorem ne_neg_of_mem_sphere

added theorem ne_neg_of_mem_unit_sphere

Modified src/analysis/normed_space/basic.lean

deleted theorem ne_neg_of_mem_sphere

deleted theorem ne_neg_of_mem_unit_sphere

Modified src/geometry/manifold/instances/sphere.lean