Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-17 05:45
44a2ae61
View on Github →
feat: port Analysis.Complex.Circle (
#4014
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Complex/Circle.lean
added
theorem
abs_coe_circle
added
def
circle.ofConjDivSelf
added
def
circle.toUnits
added
theorem
circle.toUnits_apply
added
def
circle
added
theorem
circle_def
added
theorem
coe_div_circle
added
theorem
coe_inv_circle
added
theorem
coe_inv_circle_eq_conj
added
def
expMapCircle
added
def
expMapCircleHom
added
theorem
expMapCircle_add
added
theorem
expMapCircle_apply
added
theorem
expMapCircle_neg
added
theorem
expMapCircle_sub
added
theorem
expMapCircle_zero
added
theorem
mem_circle_iff_abs
added
theorem
mem_circle_iff_normSq
added
theorem
ne_zero_of_mem_circle
added
theorem
normSq_eq_of_mem_circle
Modified
Mathlib/Analysis/Normed/Field/UnitBall.lean
Modified
Mathlib/Topology/MetricSpace/Basic.lean